NRR.Geometry.ConvexBody — the support function

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

h_K(u) = sup { ⟪x, u⟫ | x ∈ K }.

For a compact nonempty K and any direction u, the linear functional x ↦ ⟪x, u⟫ is continuous, so it attains its maximum on K; hence the supremum is finite and attained. The support function is the canonical analytic interface to a convex body: width and perimeter are later expressed through it.

Design notes

• The definition uses sSup of the image of K under x ↦ ⟪x, u⟫, matching the mathematical formula. All order-theoretic boilerplate is discharged once, via the compactness maximizer IsCompact.exists_isMaxOn, which produces an IsGreatest witness for the image; from that the sSup characterisation, the attained maximum, the upper bound, and the least-upper-bound property all follow without hand-written epsilon arguments.
• The public API (inner_le_supportFunction, supportFunction_le, exists_supportPoint, the sSup characterisation, the zero-direction value, and congruence) does not expose the implementation detail that sSup is used; downstream files can treat supportFunction through these lemmas alone.
• We follow the library convention inner ℝ x u for the real inner product.

Import policy

Following the library-wide policy, Basic.lean already pulls in import Mathlib, so no extra imports are required here. The decisive Mathlib results used are IsCompact.exists_isMaxOn, IsGreatest.csSup_eq, le_csSup, csSup_le, and continuity of the inner product.

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

The support function of a convex body K in direction u: h_K(u) = sup { ⟪x, u⟫ | x ∈ K }. For compact nonempty K the supremum is finite and attained (see exists_supportPoint).

Equations

• K.supportFunction u = sSup ((fun (x : E) => inner ℝ x u) '' K.carrier)

theorem NRR.Geometry.ConvexBody.supportFunction_eq_sSup {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] (K : ConvexBody E) (u : E) : K.supportFunction u = sSup ((fun (x : E) => inner ℝ x u) '' K.carrier)

Unfolding lemma: the support function is the supremum of the inner products over K.

theorem NRR.Geometry.ConvexBody.exists_isMaxOn_inner {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] (K : ConvexBody E) (u : E) : ∃ x ∈ K.carrier, IsMaxOn (fun (y : E) => inner ℝ y u) K.carrier x

The linear functional x ↦ ⟪x, u⟫ attains its maximum on the (compact, nonempty) body K: there is a point of K that is a maximiser. This is the compactness core of the API.

theorem NRR.Geometry.ConvexBody.exists_isGreatest_image {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] (K : ConvexBody E) (u : E) : ∃ x ∈ K.carrier, IsGreatest ((fun (x : E) => inner ℝ x u) '' K.carrier) (inner ℝ x u)

The image of K under x ↦ ⟪x, u⟫ has a greatest element, attained at a support point.

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

Existence of a support point. For every direction u there is a point of K at which the inner product equals the support function; equivalently, the supremum is attained.

theorem NRR.Geometry.ConvexBody.supportFunction_mem_image {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] (K : ConvexBody E) (u : E) : K.supportFunction u ∈ (fun (x : E) => inner ℝ x u) '' K.carrier

The support function lies in the image, i.e. is attained as an inner product.

theorem NRR.Geometry.ConvexBody.inner_le_supportFunction {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] (K : ConvexBody E) {x u : E} (hx : x ∈ K.carrier) : inner ℝ x u ≤ K.supportFunction u

Upper bound. Every inner product ⟪x, u⟫ for x ∈ K is at most the support function.

theorem NRR.Geometry.ConvexBody.supportFunction_le {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] (K : ConvexBody E) {u : E} {a : ℝ} (ha : ∀ x ∈ K.carrier, inner ℝ x u ≤ a) : K.supportFunction u ≤ a

Least upper bound. If a bounds every inner product over K, then it bounds the support function.

theorem NRR.Geometry.ConvexBody.supportFunction_congr {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] {K L : ConvexBody E} (h : K.carrier = L.carrier) (u : E) : K.supportFunction u = L.supportFunction u

Extensionality compatibility. The support function only depends on the carrier set.

@[simp]

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

Zero direction. The support function in the zero direction is zero.