noncomputable def unitDiskBoundaryExtension (φ : ↑(Metric.sphere 0 1) → ℝ) : EuclideanSpace ℝ (Fin 2) → WithTop ℝ

The textbook unit-disk boundary extension on the Euclidean plane EuclideanSpace ℝ (Fin 2): it is 0 on the open unit disk, equal to φ on the unit circle, and ⊤ outside the closed unit disk.

theorem unitDiskBoundaryExtension_eq_zero_of_norm_lt_one {φ : ↑(Metric.sphere 0 1) → ℝ} {x : EuclideanSpace ℝ (Fin 2)} (hx : ‖x‖ < 1) : unitDiskBoundaryExtension φ x = 0

On the open unit ball, unitDiskBoundaryExtension φ takes the value 0.

theorem unitDiskBoundaryExtension_eq_top_of_not_mem_closedBall {φ : ↑(Metric.sphere 0 1) → ℝ} {x : EuclideanSpace ℝ (Fin 2)} (hx : x ∉ Metric.closedBall 0 1) : unitDiskBoundaryExtension φ x = ⊤

Helper for Proposition 3.8: outside the closed unit ball, the unit-disk boundary extension takes the value ⊤.

theorem mem_dom_unitDiskBoundaryExtension_iff {φ : ↑(Metric.sphere 0 1) → ℝ} {x : EuclideanSpace ℝ (Fin 2)} : x ∈ withTopEffectiveDomain (unitDiskBoundaryExtension φ) ↔ x ∈ Metric.closedBall 0 1

Helper for Proposition 3.8: the effective domain of the unit-disk boundary extension is exactly the closed unit ball.

theorem zero_le_withTopRealPart_unitDiskBoundaryExtension {φ : ↑(Metric.sphere 0 1) → ℝ} (hφ_nonneg : ∀ (z : ↑(Metric.sphere 0 1)), 0 ≤ φ z) {x : EuclideanSpace ℝ (Fin 2)} (hx : x ∈ Metric.closedBall 0 1) : 0 ≤ withTopRealPart (unitDiskBoundaryExtension φ) x

Helper for Proposition 3.8: the real-valued representative of the unit-disk boundary extension is nonnegative on the closed unit ball whenever the boundary datum is nonnegative.

theorem unitDiskBoundaryExtension_eq_zero_of_mem_closedBall {φ : ↑(Metric.sphere 0 1) → ℝ} (hzero : ∀ (z : ↑(Metric.sphere 0 1)), φ z = 0) {x : EuclideanSpace ℝ (Fin 2)} (hx : x ∈ Metric.closedBall 0 1) : unitDiskBoundaryExtension φ x = 0

Helper for Proposition 3.8: if the boundary datum vanishes on the unit circle, then the unit-disk boundary extension vanishes on the whole closed unit ball.

theorem unitDiskBoundaryExtension_convex_and_effectiveDomain (φ : ↑(Metric.sphere 0 1) → ℝ) (hφ_nonneg : ∀ (z : ↑(Metric.sphere 0 1)), 0 ≤ φ z) : ConvexOn ℝ (withTopEffectiveDomain (unitDiskBoundaryExtension φ)) (withTopRealPart (unitDiskBoundaryExtension φ)) ∧ withTopEffectiveDomain (unitDiskBoundaryExtension φ) = Metric.closedBall 0 1

Proposition 3.8 on the Euclidean unit circle: for a nonnegative function on the unit sphere in EuclideanSpace ℝ (Fin 2), the associated extended-real-valued unit-disk boundary extension is convex in the chapter owner sense, and its effective domain is exactly the closed unit disk.

theorem unitDiskBoundaryExtension_lowerSemicontinuous_iff_eq_zero (φ : ↑(Metric.sphere 0 1) → ℝ) (hφ_nonneg : ∀ (z : ↑(Metric.sphere 0 1)), 0 ≤ φ z) : LowerSemicontinuous (unitDiskBoundaryExtension φ) ↔ ∀ (z : ↑(Metric.sphere 0 1)), φ z = 0

On EuclideanSpace ℝ (Fin 2), the unit-disk boundary extension is lower semicontinuous exactly when the boundary datum vanishes identically on the unit circle.