Domains with C¹ boundary

The extension operator asks that the boundary be C¹, and this file states that hypothesis as Evans states it (§C.1, p. 665): the boundary ∂U is C^k when for each x⁰ ∈ ∂U there are r > 0 and a C^k function γ : ℝ^{n-1} → ℝ such that, upon relabelling and reorienting the coordinate axes if necessary, U ∩ B(x⁰, r) = {x ∈ B(x⁰, r) | xₙ > γ(x₁, …, x_{n-1})}. Guo asks the same in Theorem III.2.2 (p. 20).

Two points of encoding. The relabelling and reorientation of the axes is a linear isometry of the whole space, split here between that isometry and the direction the graph is taken in. A function of the coordinates other than the j-th is a function of all of them that does not depend on the j-th, which is IndepCoord.

Nothing else is added. In particular the chart asks for no bound on the gradient of the graph, which the statements about the shear all need: exists_bounded_graph supplies one instead, by cutting the graph off in the tangential directions outside the ball the chart describes, where the chart constrains nothing.

Main declarations

• EllipticPdes.Extension.tangential: the projection killing the direction of the graph.
• EllipticPdes.Extension.exists_bound_on_cylinder: a continuous function independent of a coordinate is bounded on a cylinder around that coordinate's axis.
• EllipticPdes.Extension.exists_bounded_graph: every graph agrees on a ball with one of bounded gradient.
• EllipticPdes.Extension.C1Chart: a boundary chart.
• EllipticPdes.Extension.C1Chart.Fits: the chart describes the domain near a point.
• EllipticPdes.Extension.HasC1Boundary: every boundary point admits a chart.
• EllipticPdes.Extension.C1Chart.fits_ball: the chart read in the original coordinates.
• EllipticPdes.Extension.isCompact_frontier: the boundary of a bounded domain is compact.
• EllipticPdes.Extension.exists_finite_chart_cover: finitely many charts' balls cover the boundary.

References

James Guo, Partial Differential Equations (Course Lecture Notes), Theorem III.2.2 (p. 20) and its proof, step 2 (p. 21); L. C. Evans, Partial Differential Equations (2nd ed.), §C.1 (p. 665) and §5.4 Theorem 1 (p. 253).

The tangential projection

noncomputable def EllipticPdes.Extension.tangential {d : ℕ} (j : Fin d) : EuclideanSpace ℝ (Fin d) →L[ℝ] EuclideanSpace ℝ (Fin d)

Projection killing the j-th coordinate, the direction a chart is a graph in.

Equations

• EllipticPdes.Extension.tangential j = ContinuousLinearMap.id ℝ (EuclideanSpace ℝ (Fin d)) - ContinuousLinearMap.smulRight (EuclideanSpace.proj j) (EuclideanSpace.single j 1)

theorem EllipticPdes.Extension.tangential_apply {d : ℕ} (j : Fin d) (y : EuclideanSpace ℝ (Fin d)) : (tangential j) y = y - y.ofLp j • EuclideanSpace.single j 1

theorem EllipticPdes.Extension.tangential_coord {d : ℕ} (j : Fin d) (y : EuclideanSpace ℝ (Fin d)) (i : Fin d) : ((tangential j) y).ofLp i = if i = j then 0 else y.ofLp i

theorem EllipticPdes.Extension.tangential_add_smul {d : ℕ} (j : Fin d) (y : EuclideanSpace ℝ (Fin d)) (t : ℝ) : (tangential j) (y + t • EuclideanSpace.single j 1) = (tangential j) y

theorem EllipticPdes.Extension.norm_tangential_le {d : ℕ} (j : Fin d) (y : EuclideanSpace ℝ (Fin d)) : ‖(tangential j) y‖ ≤ ‖y‖

The projection does not increase the norm.

theorem EllipticPdes.Extension.apply_tangential {d : ℕ} {j : Fin d} {f : EuclideanSpace ℝ (Fin d) → ℝ} (hind : IndepCoord j f) (y : EuclideanSpace ℝ (Fin d)) : f ((tangential j) y) = f y

A function independent of the j-th coordinate factors through the projection.

theorem EllipticPdes.Extension.exists_bound_on_cylinder {d : ℕ} {j : Fin d} {f : EuclideanSpace ℝ (Fin d) → ℝ} (hf : Continuous f) (hind : IndepCoord j f) (z : EuclideanSpace ℝ (Fin d)) (R : ℝ) : ∃ (M : ℝ), 0 ≤ M ∧ ∀ (y : EuclideanSpace ℝ (Fin d)), ‖(tangential j) y - (tangential j) z‖ ≤ R → ‖f y‖ ≤ M

Boundedness on a cylinder of a continuous function independent of a coordinate. The function factors through the projection, so its values on the cylinder are its values on a closed ball, which is compact.

theorem EllipticPdes.Extension.norm_partialD_le_fderiv {d : ℕ} {f : EuclideanSpace ℝ (Fin d) → ℝ} (k : Fin d) (y : EuclideanSpace ℝ (Fin d)) : ‖Sobolev.partialD k f y‖ ≤ ‖fderiv ℝ f y‖

A partial derivative is bounded by the derivative, the coordinate direction being a unit vector.

Cutting a graph off outside the ball it describes

theorem EllipticPdes.Extension.exists_bounded_graph {d : ℕ} {j : Fin d} {γ : EuclideanSpace ℝ (Fin d) → ℝ} (hγ : ContDiff ℝ 1 γ) (hind : IndepCoord j γ) (z : EuclideanSpace ℝ (Fin d)) {r : ℝ} (hr : 0 < r) : ∃ (γ' : EuclideanSpace ℝ (Fin d) → ℝ) (M : ℝ), ContDiff ℝ 1 γ' ∧ IndepCoord j γ' ∧ (∀ (k : Fin d) (y : EuclideanSpace ℝ (Fin d)), ‖Sobolev.partialD k γ' y‖ ≤ M) ∧ aboveGraph j γ' ∩ Metric.ball z r = aboveGraph j γ ∩ Metric.ball z r

Every graph agrees on a ball with one of bounded gradient. A chart constrains its graph only on the ball it describes, so cutting the graph off in the tangential directions leaves the description alone and bounds the gradient. This is what lets the chart ask for no bound while every statement about the shear has one.

theorem EllipticPdes.Extension.preimage_motion_ball {d : ℕ} (e : EuclideanSpace ℝ (Fin d) ≃ₗᵢ[ℝ] EuclideanSpace ℝ (Fin d)) (x : EuclideanSpace ℝ (Fin d)) (r : ℝ) : ⇑e ⁻¹' Metric.ball (e x) r = Metric.ball x r

An isometry pulls a ball about an image point back to the ball about the point.

The boundary chart

structure EllipticPdes.Extension.C1Chart (d : ℕ) : Type

Boundary chart of class C¹. The isometry is the relabelling and reorientation of the axes, the direction is the coordinate the graph is taken in, and the radius is the size of the neighbourhood the description covers.

• motion : EuclideanSpace ℝ (Fin d) ≃ₗᵢ[ℝ] EuclideanSpace ℝ (Fin d)

  The relabelling and reorientation of the coordinate axes.

• dir : Fin d

  The coordinate the graph is taken in.

• graph : EuclideanSpace ℝ (Fin d) → ℝ

  The graph, which depends on the coordinates other than dir.

• radius : ℝ

  The radius of the neighbourhood the chart describes.

• radius_pos : 0 < self.radius

  The neighbourhood is nonempty.

• graph_contDiff : ContDiff ℝ 1 self.graph

  The graph is of class C¹.

• graph_indep : IndepCoord self.dir self.graph

  The graph does not depend on the coordinate it is a graph in.

def EllipticPdes.Extension.C1Chart.region {d : ℕ} (c : C1Chart d) : Set (EuclideanSpace ℝ (Fin d))

The region the chart describes, in the coordinates the chart puts the domain in.

Equations

• c.region = EllipticPdes.Extension.aboveGraph c.dir c.graph

def EllipticPdes.Extension.C1Chart.Fits {d : ℕ} (c : C1Chart d) (Ω : Set (EuclideanSpace ℝ (Fin d))) (x : EuclideanSpace ℝ (Fin d)) : Prop

Description of Ω near x by the chart. After the rigid motion, the domain and the region above the graph agree on the ball of the chart's radius.

Equations

• c.Fits Ω x = (⇑c.motion '' Ω ∩ Metric.ball (c.motion x) c.radius = c.region ∩ Metric.ball (c.motion x) c.radius)

theorem EllipticPdes.Extension.C1Chart.fits_ball {d : ℕ} (c : C1Chart d) {Ω : Set (EuclideanSpace ℝ (Fin d))} {x : EuclideanSpace ℝ (Fin d)} (h : c.Fits Ω x) : Ω ∩ Metric.ball x c.radius = ⇑c.motion ⁻¹' c.region ∩ Metric.ball x c.radius

Chart read in the original coordinates. On the ball about x, the domain agrees with the region above the graph pulled back through the motion.

theorem EllipticPdes.Extension.C1Chart.graph_differentiable {d : ℕ} (c : C1Chart d) : Differentiable ℝ c.graph

The graph is differentiable, being of class C¹.

theorem EllipticPdes.Extension.C1Chart.isOpen_region {d : ℕ} (c : C1Chart d) : IsOpen c.region

The region the chart describes is open.

theorem EllipticPdes.Extension.C1Chart.exists_bounded_graph {d : ℕ} (c : C1Chart d) (z : EuclideanSpace ℝ (Fin d)) : ∃ (γ' : EuclideanSpace ℝ (Fin d) → ℝ) (M : ℝ), ContDiff ℝ 1 γ' ∧ IndepCoord c.dir γ' ∧ (∀ (k : Fin d) (y : EuclideanSpace ℝ (Fin d)), ‖Sobolev.partialD k γ' y‖ ≤ M) ∧ aboveGraph c.dir γ' ∩ Metric.ball z c.radius = c.region ∩ Metric.ball z c.radius

Every chart admits a graph of bounded gradient describing the same region on its ball. The chart itself asks for no bound, as Evans' definition does not.

def EllipticPdes.Extension.HasC1Boundary {d : ℕ} (Ω : Set (EuclideanSpace ℝ (Fin d))) : Prop

Ω has C¹ boundary. Every boundary point admits a chart, which is the hypothesis of Guo's Theorem III.2.2 and of Evans' §5.4 Theorem 1.

Equations

• EllipticPdes.Extension.HasC1Boundary Ω = ∀ x ∈ frontier Ω, ∃ (c : EllipticPdes.Extension.C1Chart d), c.Fits Ω x

Instances and consequences

noncomputable def EllipticPdes.Extension.graphChart {d : ℕ} {j : Fin d} {γ : EuclideanSpace ℝ (Fin d) → ℝ} (hγ : ContDiff ℝ 1 γ) (hind : IndepCoord j γ) : C1Chart d

The chart taken by a region that is already the region above a graph: the identity motion, and any radius.

Equations

• One or more equations did not get rendered due to their size.

theorem EllipticPdes.Extension.hasC1Boundary_aboveGraph {d : ℕ} {j : Fin d} {γ : EuclideanSpace ℝ (Fin d) → ℝ} (hγ : ContDiff ℝ 1 γ) (hind : IndepCoord j γ) : HasC1Boundary (aboveGraph j γ)

C¹ boundary of the region above a graph, the identity being a chart at every point.

theorem EllipticPdes.Extension.hasC1Boundary_halfSpace {d : ℕ} (j : Fin d) : HasC1Boundary (halfSpace j)

C¹ boundary of the half space, its chart being the zero graph.

theorem EllipticPdes.Extension.isCompact_frontier {d : ℕ} {Ω : Set (EuclideanSpace ℝ (Fin d))} (hΩ : Bornology.IsBounded Ω) : IsCompact (frontier Ω)

Compactness of the boundary of a bounded domain, which is what a finite subcover of charts asks for.

theorem EllipticPdes.Extension.exists_finite_chart_cover {d : ℕ} (hd : 0 < d) {Ω : Set (EuclideanSpace ℝ (Fin d))} (hΩ : Bornology.IsBounded Ω) (hC1 : HasC1Boundary Ω) : ∃ (F : Finset (EuclideanSpace ℝ (Fin d))) (c : EuclideanSpace ℝ (Fin d) → C1Chart d), (∀ x ∈ F, x ∈ frontier Ω) ∧ (∀ x ∈ F, (c x).Fits Ω x) ∧ frontier Ω ⊆ ⋃ x ∈ F, Metric.ball x (c x).radius

Finite cover of the boundary by charts. The boundary of a bounded domain is compact and a domain with C¹ boundary has a chart at each of its points, so finitely many of the charts' balls cover it. The chart is returned as a function on the whole space, which asks the dimension to be positive: in dimension zero there is no direction for a graph to be taken in, and no chart at all.