C¹ boundary of the unit ball

Every theorem of this development on a bounded domain with C¹ boundary has, until this file, only the half space as an instance of its boundary hypothesis, and the half space is unbounded. This file supplies the unit ball, so that the extension operator, the embeddings of order k, global approximation, Rellich-Kondrachov on H¹(Ω) and the Poincaré inequality with the mean subtracted all have a domain to be applied to.

The chart at a boundary point is the reflection in the hyperplane bisecting the point and the south pole, which is a linear isometry sending the point to the pole and the ball to itself, together with the graph of the lower hemisphere, cut off in the tangential directions so that it is C¹ on the whole space and independent of the vertical coordinate. On the ball of radius one half about the pole every point has vertical coordinate below one half and tangential part of norm below one half, so the cutoff is inactive, and the ball is the region above the graph there because ‖y‖² = ‖y'‖² + y_d² with y_d < 0.

Main declarations

• EllipticPdes.Extension.norm_sq_eq_tangential_add_sq: the norm splits into the tangential part and the coordinate.
• EllipticPdes.Extension.ballGraph: the cut-off lower hemisphere.
• EllipticPdes.Extension.ballChart: the chart at a boundary point of the unit ball.
• EllipticPdes.Extension.hasC1Boundary_ball: the unit ball has C¹ boundary.

References

L. C. Evans, Partial Differential Equations (2nd ed.), §C.1 (p. 665); James Guo, Partial Differential Equations (Course Lecture Notes), Definition III.1.1.

The norm through the tangential projection

theorem EllipticPdes.Extension.norm_sq_eq_tangential_add_sq {d : ℕ} (j : Fin d) (y : EuclideanSpace ℝ (Fin d)) : ‖y‖ ^ 2 = ‖(tangential j) y‖ ^ 2 + y.ofLp j ^ 2

Norm split into the tangential part and the coordinate.

theorem EllipticPdes.Extension.tangential_neg_single {d : ℕ} (j : Fin d) : (tangential j) (-EuclideanSpace.single j 1) = 0

The south pole has no tangential part.

The graph of the lower hemisphere

noncomputable def EllipticPdes.Extension.ballBump : ContDiffBump 0

The cutoff in the tangential directions: one on [0, 1/4], zero from 1/2 on.

Equations

• EllipticPdes.Extension.ballBump = { rIn := 1 / 4, rOut := 1 / 2, rIn_pos := EllipticPdes.Extension.ballBump._proof_1, rIn_lt_rOut := EllipticPdes.Extension.ballBump._proof_2 }

theorem EllipticPdes.Extension.ballBump_mul_le {s : ℝ} (hs : 0 ≤ s) : ↑ballBump s * s ≤ 1 / 2

The argument of the square root stays above one half.

theorem EllipticPdes.Extension.ballBump_eq_one {s : ℝ} (hs : 0 ≤ s) (hs' : s ≤ 1 / 4) : ↑ballBump s = 1

The cutoff is inactive on [0, 1/4].

noncomputable def EllipticPdes.Extension.ballGraph {d : ℕ} (j : Fin d) (y : EuclideanSpace ℝ (Fin d)) : ℝ

Graph of the lower hemisphere, cut off in the tangential directions so that it is defined and C¹ on the whole space.

Equations

• EllipticPdes.Extension.ballGraph j y = -√(1 - ↑EllipticPdes.Extension.ballBump (‖(EllipticPdes.Extension.tangential j) y‖ ^ 2) * ‖(EllipticPdes.Extension.tangential j) y‖ ^ 2)

theorem EllipticPdes.Extension.ballGraph_eq_of_le {d : ℕ} (j : Fin d) {y : EuclideanSpace ℝ (Fin d)} (hy : ‖(tangential j) y‖ ^ 2 ≤ 1 / 4) : ballGraph j y = -√(1 - ‖(tangential j) y‖ ^ 2)

Near the pole the graph is the lower hemisphere itself.

theorem EllipticPdes.Extension.contDiff_ballGraph {d : ℕ} (j : Fin d) : ContDiff ℝ 1 (ballGraph j)

The graph is C¹, the square root being taken of a quantity above one half.

theorem EllipticPdes.Extension.indepCoord_ballGraph {d : ℕ} (j : Fin d) : IndepCoord j (ballGraph j)

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

The chart

noncomputable def EllipticPdes.Extension.ballChart {d : ℕ} (hd : 0 < d) (x : EuclideanSpace ℝ (Fin d)) : C1Chart d

Chart at a boundary point of the unit ball: the reflection sending the point to the south pole, the direction of the pole, the cut-off lower hemisphere, and radius one half.

Equations

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

theorem EllipticPdes.Extension.ballChart_motion_apply {d : ℕ} (hd : 0 < d) {x : EuclideanSpace ℝ (Fin d)} (hx : ‖x‖ = 1) : (ballChart hd x).motion x = -EuclideanSpace.single ⟨0, hd⟩ 1

The reflection sends the point to the pole.

theorem EllipticPdes.Extension.ballChart_fits {d : ℕ} (hd : 0 < d) {x : EuclideanSpace ℝ (Fin d)} (hx : ‖x‖ = 1) : (ballChart hd x).Fits (Metric.ball 0 1) x

Fit of the chart at its boundary point. On the ball of radius one half about the pole, membership of the unit ball is the inequality y_d > -√(1 - ‖y'‖²).

theorem EllipticPdes.Extension.hasC1Boundary_ball {d : ℕ} (hd : 0 < d) : HasC1Boundary (Metric.ball 0 1)

C¹ boundary of the unit ball. Its boundary is the unit sphere, and every point of the sphere has the chart above.