NRR.Geometry.ConvexBody — width function transformation identities

This module records how the width function w_K(u) = h_K(u) + h_K(-u) transforms under the standard operations on a ConvexBody K in a real inner product space E:

• translation invariance (widthFunction_translate),
• positive scaling of the body (widthFunction_scalePos_body),
• scaling of the direction (widthFunction_smul_direction), and
• linear isometry equivalences (widthFunction_imageLinearIsometryEquiv).

Design notes

Every identity is reduced to the corresponding support-function transformation lemma from SupportFunction.lean, SupportFunctionBasic.lean and SupportFunctionTransform.lean:

• supportFunction_translate — h_{K+a}(u) = ⟪a, u⟫ + h_K(u),
• supportFunction_scalePos_body — h_{rK}(u) = r · h_K(u) for 0 < r,
• supportFunction_smul_direction_of_nonneg — h_K(c u) = c · h_K(u) for 0 ≤ c,
• supportFunction_imageLinearIsometryEquiv — h_{eK}(u) = h_K(e⁻¹ u).

No structure internals or sSup are unfolded here.

Import policy

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

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

Translation invariance. The width is unchanged under translating the body.

theorem NRR.Geometry.ConvexBody.widthFunction_scalePos_body {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] (K : ConvexBody E) {r : ℝ} (hr : 0 < r) (u : E) : (K.scalePos r hr).widthFunction u = r * K.widthFunction u

Positive scaling of the body. w_{rK}(u) = r · w_K(u) for 0 < r.

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

Direction scaling. w_K(c u) = |c| · w_K(u) for any real c.

theorem NRR.Geometry.ConvexBody.widthFunction_imageLinearIsometryEquiv {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] {F : Type u_2} [NormedAddCommGroup F] [InnerProductSpace ℝ F] (K : ConvexBody E) (e : E ≃ₗᵢ[ℝ] F) (u : F) : (K.imageLinearIsometryEquiv e).widthFunction u = K.widthFunction (e.symm u)

Image under a linear isometry equivalence. w_{eK}(u) = w_K(e⁻¹ u).