NRR.Geometry.ConvexBody — translations and positive scalings

This module provides a reusable API for translations K.translate v and positive scalings K.scalePos r hr of solid convex bodies over a real normed vector space.

The two constructors are

• ConvexBody.translate K v : ConvexBody E with carrier (fun x => v + x) '' K;
• ConvexBody.scalePos K r hr : ConvexBody E with carrier (fun x => r • x) '' K (requiring 0 < r, so that scaling is a homeomorphism preserving the interior).

together with carrier/membership simp lemmas, the identity/composition laws, and the translation–scaling interaction.

Why 0 < r

Scaling by r = 0 collapses everything to a point and destroys the nonempty-interior (solidity) field of a ConvexBody; it is therefore excluded. For any r ≠ 0 scaling is a homeomorphism (Homeomorph.smulOfNeZero), and we specialise to the positive case as required by the downstream width / support-function development.

Mathlib lemmas reused

• Convex.translate, Convex.smul — convexity of translates and scalings.
• IsCompact.image, continuous_const_smul, continuous_add — compactness of images.
• Homeomorph.addLeft, Homeomorph.smulOfNeZero, Homeomorph.image_interior — interior preservation.
• Set.image_smul, Set.image_image — carrier bookkeeping.

Import policy

Following the library-wide policy, Basic.lean already pulls in import Mathlib, so no extra imports are required here.

Translation

def NRR.Geometry.ConvexBody.translate {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] (K : ConvexBody E) (v : E) : ConvexBody E

The translate of a convex body by a vector v, as a convex body with carrier (fun x => v + x) '' K. Translation is a homeomorphism, so solidity is preserved.

Equations

• K.translate v = { carrier := (fun (x : E) => v + x) '' K.carrier, convex' := ⋯, isCompact' := ⋯, interior_nonempty' := ⋯ }

@[simp]

theorem NRR.Geometry.ConvexBody.translate_carrier {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] (K : ConvexBody E) (v : E) : (K.translate v).carrier = (fun (x : E) => v + x) '' K.carrier

theorem NRR.Geometry.ConvexBody.mem_translate {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] (K : ConvexBody E) (v x : E) : x ∈ (K.translate v).carrier ↔ x - v ∈ K.carrier

@[simp]

theorem NRR.Geometry.ConvexBody.translate_zero {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] (K : ConvexBody E) : K.translate 0 = K

theorem NRR.Geometry.ConvexBody.translate_translate {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] (K : ConvexBody E) (v w : E) : (K.translate v).translate w = K.translate (w + v)

Positive scaling

def NRR.Geometry.ConvexBody.scalePos {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] (K : ConvexBody E) (r : ℝ) (hr : 0 < r) : ConvexBody E

The positive scaling of a convex body by r > 0, as a convex body with carrier (fun x => r • x) '' K. Scaling by a nonzero scalar is a homeomorphism, so solidity is preserved.

Equations

• K.scalePos r hr = { carrier := (fun (x : E) => r • x) '' K.carrier, convex' := ⋯, isCompact' := ⋯, interior_nonempty' := ⋯ }

@[simp]

theorem NRR.Geometry.ConvexBody.scalePos_carrier {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] (K : ConvexBody E) {r : ℝ} (hr : 0 < r) : (K.scalePos r hr).carrier = (fun (x : E) => r • x) '' K.carrier

theorem NRR.Geometry.ConvexBody.mem_scalePos {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] (K : ConvexBody E) {r : ℝ} (hr : 0 < r) (x : E) : x ∈ (K.scalePos r hr).carrier ↔ r⁻¹ • x ∈ K.carrier

@[simp]

theorem NRR.Geometry.ConvexBody.scalePos_one {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] (K : ConvexBody E) : K.scalePos 1 ⋯ = K

theorem NRR.Geometry.ConvexBody.scalePos_scalePos {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] (K : ConvexBody E) {r s : ℝ} (hr : 0 < r) (hs : 0 < s) : (K.scalePos r hr).scalePos s hs = K.scalePos (s * r) ⋯

Interaction of scaling and translation

theorem NRR.Geometry.ConvexBody.scalePos_translate {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] (K : ConvexBody E) {r : ℝ} (hr : 0 < r) (v : E) : (K.translate v).scalePos r hr = (K.scalePos r hr).translate (r • v)