NRR.Geometry.ConvexBody — the width function

This module introduces the width function of a ConvexBody K in a real inner product space E:

w_K(u) = h_K(u) + h_K(-u),

defined on all vectors u, not only unit vectors. Geometrically, w_K(u) measures the extent of K in the direction u (the distance between the two supporting hyperplanes with outer normals u and -u, scaled by ‖u‖).

Design notes

• The width function is built directly on top of the support-function interface (supportFunction, inner_le_supportFunction, supportFunction_mono, supportFunction_smul_direction_of_nonneg) from SupportFunction.lean and SupportFunctionBasic.lean. No sSup or structure internals are unfolded here.
• The basic algebraic properties are: evenness (widthFunction_neg), vanishing at zero (widthFunction_zero), nonnegativity (widthFunction_nonneg), monotonicity (widthFunction_mono), and positive homogeneity (widthFunction_smul_direction_of_nonneg).

Import policy

SupportFunction.lean (via Basic.lean) already pulls in import Mathlib, so no extra imports are required here.

noncomputable def NRR.Geometry.ConvexBody.widthFunction {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] (K : ConvexBody E) (u : E) : ℝ

The width function of a convex body K in direction u: w_K(u) = h_K(u) + h_K(-u). Defined for all vectors u, not only unit vectors.

Equations

• K.widthFunction u = K.supportFunction u + K.supportFunction (-u)

@[simp]

theorem NRR.Geometry.ConvexBody.widthFunction_def {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] (K : ConvexBody E) (u : E) : K.widthFunction u = K.supportFunction u + K.supportFunction (-u)

Unfolding lemma for the width function.

theorem NRR.Geometry.ConvexBody.widthFunction_neg {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] (K : ConvexBody E) (u : E) : K.widthFunction (-u) = K.widthFunction u

Evenness. The width function is invariant under negation of the direction.

theorem NRR.Geometry.ConvexBody.widthFunction_zero {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] (K : ConvexBody E) : K.widthFunction 0 = 0

Zero direction. The width function vanishes in the zero direction.

theorem NRR.Geometry.ConvexBody.widthFunction_nonneg {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] (K : ConvexBody E) (u : E) : 0 ≤ K.widthFunction u

Nonnegativity. The width function is always nonnegative.

theorem NRR.Geometry.ConvexBody.widthFunction_mono {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] {K L : ConvexBody E} (hKL : K.carrier ⊆ L.carrier) (u : E) : K.widthFunction u ≤ L.widthFunction u

Monotonicity. A larger body has a larger width in every direction.

theorem NRR.Geometry.ConvexBody.widthFunction_smul_direction_of_nonneg {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] (K : ConvexBody E) {c : ℝ} (hc : 0 ≤ c) (u : E) : K.widthFunction (c • u) = c * K.widthFunction u

Positive homogeneity (nonnegative scalar). w_K(c u) = c · w_K(u) for 0 ≤ c.