NRR.Geometry.ConvexBody — continuity of the support function

This module proves that the support function u ↦ h_K(u) of a ConvexBody K is (globally Lipschitz, hence) continuous in the direction variable. This is the analytic prerequisite for width, Cauchy perimeter, and all later integration over the unit circle / sphere.

Contents

• exists_radius_bound — existence of a radius R ≥ 0 bounding the norms of points of K (from compactness / boundedness).
• supportFunction_lipschitz_with_radius — the quantitative estimate |h_K(u) - h_K(v)| ≤ R · ‖u - v‖ whenever K ⊆ closedBall 0 R.
• supportFunction_lipschitzWith — the bundled LipschitzWith statement.
• continuous_supportFunction, continuousAt_supportFunction, continuousOn_supportFunction — full-space continuity.
• uniformContinuousOn_supportFunction — uniform continuity on any subset (in fact the global Lipschitz bound gives uniform continuity everywhere).
• continuousOn_supportFunction_on_sphere — continuity restricted to the unit sphere, an immediate corollary.

Design notes

The proof follows the preferred Lipschitz route: subadditivity of the support function plus the radius bound h_K(u) ≤ R‖u‖ give h_K(u) - h_K(v) ≤ h_K(u - v) ≤ R‖u - v‖, and symmetrically, so the map is R-Lipschitz. This is more robust than a compact-maximum-with-parameters argument and yields the strongest downstream API.

theorem NRR.Geometry.ConvexBody.exists_radius_bound {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] (K : ConvexBody E) : ∃ (R : ℝ), 0 ≤ R ∧ ∀ x ∈ K.carrier, ‖x‖ ≤ R

Existence of a radius bound. Every convex body is bounded, so there is R ≥ 0 with ‖x‖ ≤ R for all x ∈ K.

theorem NRR.Geometry.ConvexBody.supportFunction_lipschitz_with_radius {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] (K : ConvexBody E) {R : ℝ} (hR : ∀ x ∈ K.carrier, ‖x‖ ≤ R) (u v : E) : |K.supportFunction u - K.supportFunction v| ≤ R * ‖u - v‖

Lipschitz estimate. If every point of K has norm at most R, the support function is R-Lipschitz: |h_K(u) - h_K(v)| ≤ R · ‖u - v‖.

theorem NRR.Geometry.ConvexBody.supportFunction_lipschitzWith {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] (K : ConvexBody E) {R : ℝ} (hRnn : 0 ≤ R) (hR : ∀ x ∈ K.carrier, ‖x‖ ≤ R) : LipschitzWith R.toNNReal fun (u : E) => K.supportFunction u

Bundled Lipschitz. The support function is R.toNNReal-Lipschitz when K ⊆ closedBall 0 R.

theorem NRR.Geometry.ConvexBody.continuous_supportFunction {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] (K : ConvexBody E) : Continuous fun (u : E) => K.supportFunction u

Full-space continuity of the support function in the direction variable.

theorem NRR.Geometry.ConvexBody.continuousAt_supportFunction {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] (K : ConvexBody E) (u : E) : ContinuousAt (fun (v : E) => K.supportFunction v) u

Continuity at a point.

theorem NRR.Geometry.ConvexBody.continuousOn_supportFunction {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] (K : ConvexBody E) (s : Set E) : ContinuousOn (fun (u : E) => K.supportFunction u) s

Continuity on a set.

theorem NRR.Geometry.ConvexBody.uniformContinuousOn_supportFunction {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] (K : ConvexBody E) {s : Set E} : UniformContinuousOn (fun (u : E) => K.supportFunction u) s

Uniform continuity on a subset. The global Lipschitz bound gives uniform continuity on every subset of the ambient inner product space.

theorem NRR.Geometry.ConvexBody.continuousOn_supportFunction_on_sphere {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] (K : ConvexBody E) : ContinuousOn (fun (u : E) => K.supportFunction u) (Metric.sphere 0 1)

Continuity on the unit sphere, an immediate corollary of full-space continuity.