The hemispheres of the unit sphere of WithLp 2 (E × ℝ) as graphs

Let E be a real normed space, say E = ℝᵏ⁺¹. The closed upper and lower hemispheres of the unit sphere S^(k+1) of the L² product WithLp 2 (E × ℝ) are the graphs of u ↦ ±√(1 - ‖u‖ ^ 2) over the closed unit ball D^(k+1) of E. For a sign c (that is, c ^ 2 = 1), TauCeti.prodHemisphereGraph sends a point u of the ball to (u, c √(1 - ‖u‖ ^ 2)). Each hemisphere is a closed embedding of the ball, the two hemispheres cover the sphere, agree on the equator ‖u‖ = 1, and meet only there.

For E = ℂ, moved into ℝ³ by the linear isometry (u, t) ↦ (Re u, Im u, t), these are the hemispheres TauCeti.hemisphereGraph of S² ⊆ ℝ³ over the closed unit disc of ℂ.

Main definitions

• TauCeti.prodHemisphereGraphPoint c u: the point (u, c √(1 - ‖u‖ ^ 2)) of WithLp 2 (E × ℝ).
• TauCeti.prodHemisphereGraph hc: the hemisphere of sign c of the unit sphere of WithLp 2 (E × ℝ), as a map from the closed unit ball of E.

Main results

• TauCeti.isClosedEmbedding_prodHemisphereGraph: each hemisphere is a closed embedding of the closed unit ball.
• TauCeti.eq_of_prodHemisphereGraph_eq: a point of a hemisphere determines the point of the ball.
• TauCeti.prodHemisphereGraph_eq_of_norm_eq_one: the hemispheres agree on the equator.
• TauCeti.norm_eq_one_of_prodHemisphereGraph_eq: hemispheres of opposite signs meet only over the boundary of the ball.
• TauCeti.exists_prodHemisphereGraph_eq: every point of the unit sphere lies on the hemisphere of the sign of its last coordinate.

noncomputable def TauCeti.prodHemisphereGraphPoint {E : Type u_1} [SeminormedAddCommGroup E] (c : ℝ) (u : E) : WithLp 2 (E × ℝ)

The point (u, c √(1 - ‖u‖ ^ 2)) of WithLp 2 (E × ℝ); for c = 1 and c = -1 and u in the closed unit ball this is the upper and the lower hemisphere of the unit sphere.

theorem TauCeti.prodHemisphereGraphPoint_def {E : Type u_1} [SeminormedAddCommGroup E] (c : ℝ) (u : E) : prodHemisphereGraphPoint c u = WithLp.toLp 2 (u, c * √(1 - ‖u‖ ^ 2))

TauCeti.prodHemisphereGraphPoint c u is the point (u, c √(1 - ‖u‖ ^ 2)).

@[simp]

theorem TauCeti.prodHemisphereGraphPoint_fst {E : Type u_1} [SeminormedAddCommGroup E] (c : ℝ) (u : E) : (prodHemisphereGraphPoint c u).fst = u

The first component of TauCeti.prodHemisphereGraphPoint c u is u.

@[simp]

theorem TauCeti.prodHemisphereGraphPoint_snd {E : Type u_1} [SeminormedAddCommGroup E] (c : ℝ) (u : E) : (prodHemisphereGraphPoint c u).snd = c * √(1 - ‖u‖ ^ 2)

The last coordinate of TauCeti.prodHemisphereGraphPoint c u is c √(1 - ‖u‖ ^ 2).

theorem TauCeti.prodHemisphereGraphPoint_mem_sphere {E : Type u_1} [SeminormedAddCommGroup E] {c : ℝ} (hc : c ^ 2 = 1) (u : ↑(Metric.closedBall 0 1)) : prodHemisphereGraphPoint c ↑u ∈ Metric.sphere 0 1

For a sign c, the points TauCeti.prodHemisphereGraphPoint c u over the closed unit ball lie on the unit sphere.

noncomputable def TauCeti.prodHemisphereGraph {E : Type u_1} [SeminormedAddCommGroup E] {c : ℝ} (hc : c ^ 2 = 1) (u : ↑(Metric.closedBall 0 1)) : ↑(Metric.sphere 0 1)

The hemisphere of sign c of the unit sphere of WithLp 2 (E × ℝ), the graph of u ↦ c √(1 - ‖u‖ ^ 2) over the closed unit ball of E.

@[simp]

theorem TauCeti.coe_prodHemisphereGraph_apply {E : Type u_1} [SeminormedAddCommGroup E] {c : ℝ} (hc : c ^ 2 = 1) (u : ↑(Metric.closedBall 0 1)) : ↑(prodHemisphereGraph hc u) = prodHemisphereGraphPoint c ↑u

TauCeti.prodHemisphereGraph hc u is the point TauCeti.prodHemisphereGraphPoint c u.

theorem TauCeti.continuous_prodHemisphereGraph {E : Type u_1} [SeminormedAddCommGroup E] {c : ℝ} (hc : c ^ 2 = 1) : Continuous (prodHemisphereGraph hc)

The hemisphere graphs are continuous.

theorem TauCeti.eq_of_prodHemisphereGraph_eq {E : Type u_1} [SeminormedAddCommGroup E] {c c' : ℝ} {hc : c ^ 2 = 1} {hc' : c' ^ 2 = 1} {u v : ↑(Metric.closedBall 0 1)} (h : prodHemisphereGraph hc u = prodHemisphereGraph hc' v) : u = v

The first component of a point of a hemisphere recovers the point of the ball, whatever the signs of the two hemispheres.

theorem TauCeti.prodHemisphereGraph_injective {E : Type u_1} [SeminormedAddCommGroup E] {c : ℝ} (hc : c ^ 2 = 1) : Function.Injective (prodHemisphereGraph hc)

Each hemisphere graph is injective.

theorem TauCeti.prodHemisphereGraph_eq_of_norm_eq_one {E : Type u_1} [SeminormedAddCommGroup E] {c c' : ℝ} (hc : c ^ 2 = 1) (hc' : c' ^ 2 = 1) {u : ↑(Metric.closedBall 0 1)} (hu : ‖↑u‖ = 1) : prodHemisphereGraph hc u = prodHemisphereGraph hc' u

The hemispheres of any two signs agree on the equator.

theorem TauCeti.norm_eq_one_of_prodHemisphereGraph_eq {E : Type u_1} [SeminormedAddCommGroup E] {c c' : ℝ} {hc : c ^ 2 = 1} {hc' : c' ^ 2 = 1} (hcc' : c ≠ c') {u v : ↑(Metric.closedBall 0 1)} (h : prodHemisphereGraph hc u = prodHemisphereGraph hc' v) : ‖↑v‖ = 1

Hemispheres of opposite signs meet only over the boundary of the ball.

theorem TauCeti.exists_prodHemisphereGraph_eq {E : Type u_1} [SeminormedAddCommGroup E] {c : ℝ} (hc : c ^ 2 = 1) (x : ↑(Metric.sphere 0 1)) (hx : 0 ≤ c * (↑x).snd) : ∃ (u : ↑(Metric.closedBall 0 1)), prodHemisphereGraph hc u = x

Every point x of the unit sphere of WithLp 2 (E × ℝ) with 0 ≤ c x.snd lies on the hemisphere of sign c, over the point x.fst of the ball.

theorem TauCeti.isClosedEmbedding_prodHemisphereGraph {E : Type u_1} [NormedAddCommGroup E] {c : ℝ} (hc : c ^ 2 = 1) : Topology.IsClosedEmbedding (prodHemisphereGraph hc)

Each hemisphere graph is a closed embedding of the closed unit ball into the unit sphere of WithLp 2 (E × ℝ); its left inverse is the projection to the first component.