NRR.Geometry.ConvexBody — support-function transformation API

This module completes the transformation API for the support function of a ConvexBody under

• translations K.translate a,
• positive scalings K.scalePos r hr,
• negation / reflection K.neg,
• linear isometry equivalences K.imageLinearIsometryEquiv e, and
• general continuous linear equivalences K.imageLinearEquiv e (via the adjoint).

The goal is that later width and perimeter proofs become pure rewriting.

Contents

• supportFunction_scalePos_body (@[simp]) — h_{rK}(u) = r · h_K(u) for 0 < r, the transformation-API spelling of the base-module lemma supportFunction_scalePos.
• ConvexBody.neg, with carrier/membership simp lemmas, and supportFunction_neg_body (@[simp]) — h_{-K}(u) = h_K(-u).
• ConvexBody.imageLinearIsometryEquiv, with carrier/membership simp lemmas, and supportFunction_imageLinearIsometryEquiv — h_{eK}(u) = h_K(e⁻¹ u).
• supportFunction_imageLinearEquiv_adjoint — h_{eK}(u) = h_K(eᵀ u) for a general continuous linear equivalence, the transformation-API spelling of the base-module lemma supportFunction_imageLinearEquiv.

Reused results

• Translation is already provided by supportFunction_translate in NRR.Geometry.ConvexBody.SupportFunctionBasic (h_{K+a}(u) = ⟪a, u⟫ + h_K(u)); it is re-exported through this module's imports and needs no restatement here.
• The base-module lemmas supportFunction_scalePos and supportFunction_imageLinearEquiv are wrapped under the transformation-API names required by This module.

Design notes

All proofs go through the order-theoretic interfaces inner_le_supportFunction (upper bound) and supportFunction_le (least upper bound), together with the attainment lemma exists_supportPoint; no sSup is manipulated directly.

For an inner product space the correct direction-pullback under a linear equivalence is the adjoint, not e.symm. For a linear isometry equivalence the adjoint coincides with e.symm, which is why the clean e.symm formula is available (and proved directly from LinearIsometryEquiv.inner_map_map, needing no completeness hypothesis). The general imageLinearEquiv formula uses ContinuousLinearMap.adjoint and hence requires the spaces to be complete (automatic in finite dimensions).

Import policy

Only SupportFunctionBasic is imported; it transitively provides the whole ConvexBody, support-function, AffineOps and LinearImage API (and, through Basic, import Mathlib).

Translation (re-exported)

The translation identity supportFunction (K.translate a) u = ⟪a, u⟫ + supportFunction K u is NRR.Geometry.ConvexBody.supportFunction_translate, proved in SupportFunctionBasic and available through this module's imports. It is not restated here to avoid a duplicate declaration.

Positive scaling of the body

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

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

This is the transformation-API spelling of the base-module lemma supportFunction_scalePos.

Negation / reflection

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

The reflection -K of a convex body through the origin, as a convex body with carrier (-·) '' K = -K. Implemented as the image under the negation linear isometry equivalence, so solidity is preserved.

Equations

• K.neg = { carrier := Neg.neg '' K.carrier, convex' := ⋯, isCompact' := ⋯, interior_nonempty' := ⋯ }

@[simp]

theorem NRR.Geometry.ConvexBody.neg_carrier {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] (K : ConvexBody E) : K.neg.carrier = Neg.neg '' K.carrier

theorem NRR.Geometry.ConvexBody.mem_neg {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] (K : ConvexBody E) (x : E) : x ∈ K.neg.carrier ↔ -x ∈ K.carrier

@[simp]

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

Reflection. h_{-K}(u) = h_K(-u).

Linear isometry equivalence

def NRR.Geometry.ConvexBody.imageLinearIsometryEquiv {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] {F : Type u_2} [NormedAddCommGroup F] [InnerProductSpace ℝ F] (K : ConvexBody E) (e : E ≃ₗᵢ[ℝ] F) : ConvexBody F

The image of a convex body under a linear isometry equivalence e : E ≃ₗᵢ[ℝ] F, as a convex body with carrier e '' K. Implemented as the image under the underlying continuous linear equivalence e.toContinuousLinearEquiv.

Equations

• K.imageLinearIsometryEquiv e = K.imageLinearEquiv ↑e

@[simp]

theorem NRR.Geometry.ConvexBody.imageLinearIsometryEquiv_carrier {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] {F : Type u_2} [NormedAddCommGroup F] [InnerProductSpace ℝ F] (K : ConvexBody E) (e : E ≃ₗᵢ[ℝ] F) : (K.imageLinearIsometryEquiv e).carrier = ⇑e '' K.carrier

theorem NRR.Geometry.ConvexBody.mem_imageLinearIsometryEquiv {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] {F : Type u_2} [NormedAddCommGroup F] [InnerProductSpace ℝ F] (K : ConvexBody E) (e : E ≃ₗᵢ[ℝ] F) (y : F) : y ∈ (K.imageLinearIsometryEquiv e).carrier ↔ e.symm y ∈ K.carrier

theorem NRR.Geometry.ConvexBody.supportFunction_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).supportFunction u = K.supportFunction (e.symm u)

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

Unlike a general linear equivalence, an isometry pulls the direction back through e.symm, because the adjoint of a linear isometry equivalence is its inverse. No completeness hypothesis is required.

General continuous linear equivalence (adjoint form)

theorem NRR.Geometry.ConvexBody.supportFunction_imageLinearEquiv_adjoint {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] {F : Type u_2} [NormedAddCommGroup F] [InnerProductSpace ℝ F] [CompleteSpace E] [CompleteSpace F] (K : ConvexBody E) (e : E ≃L[ℝ] F) (u : F) : (K.imageLinearEquiv e).supportFunction u = K.supportFunction ((ContinuousLinearMap.adjoint ↑e) u)

Image under a continuous linear equivalence (adjoint form). h_{eK}(u) = h_K(eᵀ u), where eᵀ = ContinuousLinearMap.adjoint (e : E →L[ℝ] F).

This is the transformation-API spelling of the base-module lemma supportFunction_imageLinearEquiv. The naive e.symm form is false unless e is an isometry (compare supportFunction_imageLinearIsometryEquiv). Completeness of E and F is required for the adjoint to exist (automatic in finite dimensions).

Reflection via the linear isometry API

For completeness we record that K.neg is the image of K under the negation linear isometry equivalence, so the reflection identity is a special case of the isometry identity.

theorem NRR.Geometry.ConvexBody.neg_eq_imageLinearIsometryEquiv_neg {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] (K : ConvexBody E) : K.neg = K.imageLinearIsometryEquiv (LinearIsometryEquiv.neg ℝ)