NRR.Geometry.ConvexBody — algebraic and geometric properties of the support function

This module strengthens the support-function API introduced in NRR.Geometry.ConvexBody.SupportFunction. It provides the properties needed for the later development of width, perimeter, and transformations of convex bodies, so that downstream files never have to reason directly with sSup.

Contents

• Attainment / support points — exists_supportPoint (re-exposed from the base module) and supportFunction_isMax.
• Positive homogeneity — supportFunction_smul_direction_of_nonneg (@[simp]) and its strictly-positive variant supportFunction_smul_direction_of_pos.
• Subadditivity — supportFunction_add_direction_le.
• Monotonicity — supportFunction_mono.
• Translation — supportFunction_translate (@[simp]).
• Scaling — supportFunction_scalePos (@[simp]).
• Linear equivalence — supportFunction_imageLinearEquiv, stated via the adjoint ContinuousLinearMap.adjoint, which is the mathematically correct direction for an inner product space (the naive e.symm form is false unless e is an isometry).
• Boundedness estimates — supportFunction_le_radius and supportFunction_abs_le.

Design notes

All proofs go through the two order-theoretic interfaces from the base module, inner_le_supportFunction (upper bound) and supportFunction_le (least upper bound), together with the attainment lemma exists_supportPoint. No sSup appears in any statement here.

For homogeneity, subadditivity, monotonicity, translation and scaling the ambient space is only assumed to be a real inner product space. The linear-equivalence lemma additionally requires the domain and codomain to be complete (so that the adjoint exists); this is automatic in finite dimensions.

Attainment and support points

theorem NRR.Geometry.ConvexBody.supportFunction_isMax {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] (K : ConvexBody E) (u : E) : ∃ x ∈ K.carrier, inner ℝ x u = K.supportFunction u ∧ ∀ y ∈ K.carrier, inner ℝ y u ≤ inner ℝ x u

Support maximiser. For every direction u there is a point of K attaining the support function, and it is a maximiser of x ↦ ⟪x, u⟫ over K.

Positive homogeneity

@[simp]

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

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

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

Positive homogeneity (positive scalar). h_K(c u) = c · h_K(u) for 0 < c.

Subadditivity

theorem NRR.Geometry.ConvexBody.supportFunction_add_direction_le {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] (K : ConvexBody E) (u v : E) : K.supportFunction (u + v) ≤ K.supportFunction u + K.supportFunction v

Subadditivity in the direction. h_K(u + v) ≤ h_K(u) + h_K(v). Note that equality does not hold in general.

Monotonicity

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

Monotonicity. A larger body has a larger support function in every direction.

Translation

@[simp]

theorem NRR.Geometry.ConvexBody.supportFunction_translate {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] (K : ConvexBody E) (a u : E) : (K.translate a).supportFunction u = inner ℝ a u + K.supportFunction u

Translation. h_{K + a}(u) = ⟪a, u⟫ + h_K(u).

Scaling

@[simp]

theorem NRR.Geometry.ConvexBody.supportFunction_scalePos {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. h_{r K}(u) = r · h_K(u) for 0 < r.

Linear equivalence

For an inner product space the correct pullback of the direction is through the adjoint of the linear map, not e.symm. We state and prove the mathematically correct identity h_{eK}(u) = h_K(eᵀ u), where eᵀ = ContinuousLinearMap.adjoint (e : E →L[ℝ] F). This requires E and F to be complete inner product spaces (automatic in finite dimensions).

theorem NRR.Geometry.ConvexBody.supportFunction_imageLinearEquiv {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. h_{eK}(u) = h_K(eᵀ u), where eᵀ is the adjoint of e.

Boundedness estimates

theorem NRR.Geometry.ConvexBody.supportFunction_le_radius {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] (K : ConvexBody E) {R : ℝ} (hR : ∀ x ∈ K.carrier, ‖x‖ ≤ R) (u : E) : K.supportFunction u ≤ R * ‖u‖

Radius bound. If every point of K has norm at most R, then h_K(u) ≤ R ‖u‖.

theorem NRR.Geometry.ConvexBody.supportFunction_abs_le {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] (K : ConvexBody E) : ∃ (C : ℝ), 0 ≤ C ∧ ∀ (u : E), |K.supportFunction u| ≤ C * ‖u‖

Uniform bound. There is a constant C ≥ 0 with |h_K(u)| ≤ C ‖u‖ for all directions u. This is the estimate needed for continuity/integrability of the support function.