NRR.Geometry.ConvexBody — continuity of the width function

This module proves that the width function u ↦ w_K(u) = h_K(u) + h_K(-u) of a ConvexBody K in a real inner product space E is continuous in the direction variable, and gives the quantitative Lipschitz estimate.

Contents

• continuous_widthFunction — full-space continuity of u ↦ w_K(u).
• continuousAt_widthFunction — continuity at a point.
• continuousOn_widthFunction — continuity on a set.
• widthFunction_lipschitz_with_radius — the quantitative estimate |w_K(u) - w_K(v)| ≤ (2 R) · ‖u - v‖ whenever ‖x‖ ≤ R for all x ∈ K.

Design notes

Everything is built on the support-function continuity and Lipschitz results from SupportFunctionContinuity.lean. Continuity follows since w_K is the sum of h_K and its composition with the (continuous) negation map. The Lipschitz estimate applies the support function estimate to u, v and to -u, -v, and adds; the two ‖·‖ terms coincide since ‖(-u) - (-v)‖ = ‖u - v‖.

Import policy

Width.lean and SupportFunctionContinuity.lean (via Basic.lean) already pull in import Mathlib, so no extra imports are required here.

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

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

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

Continuity at a point.

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

Continuity on a set.

theorem NRR.Geometry.ConvexBody.widthFunction_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.widthFunction u - K.widthFunction v| ≤ 2 * R * ‖u - v‖

Lipschitz estimate. If every point of K has norm at most R, the width function satisfies |w_K(u) - w_K(v)| ≤ (2 R) · ‖u - v‖.