NRR.BodySpace — joint support-function and width continuity

This module proves that support functions and widths depend continuously on both the body and the direction, for bodies varying in the fixed-parent hyperspace ConvexSubbody K and in the lower-area subspace BodySpace K A.

Core reusable lemma

The heart of the file is a body-parameter continuity criterion for the solid geometry bodies: if a family K : α → Geometry.ConvexBody Plane is continuous for the Hausdorff-metric topology, then it is a SupportFunctionContinuousFamily and a WidthContinuousFamily. The proof follows the standard split of h_{K a}(u) - h_{K a₀}(u₀) into a body-variation term, controlled by the Hausdorff–Lipschitz estimate abs_supportFunction_sub_le_hausdorffDist_mul_norm, and a direction-variation term, controlled by the fixed-body direction continuity continuous_supportFunction.

Possibly-degenerate subbodies

The project support function Geometry.ConvexBody.supportFunction is defined only on the solid bundled type Geometry.ConvexBody, whereas a ConvexSubbody K may be lower-dimensional. We therefore work with the support function of the underlying compact convex set directly — the same sSup ⟪·, u⟫ formula as Geometry.ConvexBody.supportFunction, now for a possibly-degenerate carrier — packaged as ConvexSubbody.supportFunction. It agrees with the geometry support function whenever the subbody is solid. Its joint continuity uses the Hausdorff–Lipschitz estimate (whose proof needs only carrier compactness and nonemptiness) and the fixed-body direction continuity, both re-established here at the set level.

Positive lower area

When A > 0 every element of BodySpace K A is genuinely solid, so the solid bridge BodySpace.toGeometryConvexBody lands in Geometry.ConvexBody Plane; the solid family predicates follow from the core reusable lemma applied to the continuous bridge BodySpace.continuous_toGeometryConvexBody.

theorem NRR.Geometry.ConvexBody.SupportFunctionContinuousFamily.of_continuous {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] {α : Type u_2} [TopologicalSpace α] {K : α → ConvexBody E} (hK : Continuous K) : SupportFunctionContinuousFamily K

theorem NRR.Geometry.ConvexBody.WidthContinuousFamily.of_continuous {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] {α : Type u_2} [TopologicalSpace α] {K : α → ConvexBody E} (hK : Continuous K) : WidthContinuousFamily K

Body-parameter width continuity for a Hausdorff-continuous family of solid bodies.

noncomputable def NRR.ConvexSubbody.supportFunction {K : Geometry.ConvexBody Geometry.Plane} (C : ConvexSubbody K) (u : Geometry.Plane) : ℝ

Support function of a convex subbody. The supremum of ⟪x, u⟫ over the (compact, nonempty) carrier of C. This is the same formula as Geometry.ConvexBody.supportFunction, valid for a possibly-degenerate carrier; it agrees with the geometry support function on solid subbodies.

Equations

• C.supportFunction u = sSup ((fun (x : NRR.Geometry.Plane) => inner ℝ x u) '' ↑C.body)

theorem NRR.ConvexSubbody.supportFunction_eq_sSup {K : Geometry.ConvexBody Geometry.Plane} (C : ConvexSubbody K) (u : Geometry.Plane) : C.supportFunction u = sSup ((fun (x : Geometry.Plane) => inner ℝ x u) '' ↑C.body)

Unfolding lemma for the subbody support function.

theorem NRR.ConvexSubbody.inner_image_bddAbove {K : Geometry.ConvexBody Geometry.Plane} (C : ConvexSubbody K) (u : Geometry.Plane) : BddAbove ((fun (x : Geometry.Plane) => inner ℝ x u) '' ↑C.body)

The image {⟪x, u⟫ | x ∈ C} is bounded above (the carrier is compact, hence bounded).

theorem NRR.ConvexSubbody.exists_supportPoint {K : Geometry.ConvexBody Geometry.Plane} (C : ConvexSubbody K) (u : Geometry.Plane) : ∃ x ∈ ↑C.body, C.supportFunction u = inner ℝ x u

Support point. The supremum defining h_C(u) is attained at some point of the carrier.

theorem NRR.ConvexSubbody.inner_le_supportFunction {K : Geometry.ConvexBody Geometry.Plane} (C : ConvexSubbody K) {x u : Geometry.Plane} (hx : x ∈ ↑C.body) : inner ℝ x u ≤ C.supportFunction u

Every point of the carrier gives an inner product bounded by the support function.

theorem NRR.ConvexSubbody.supportFunction_eq_geometry {K : Geometry.ConvexBody Geometry.Plane} (C : ConvexSubbody K) (G : Geometry.ConvexBody Geometry.Plane) (h : ↑C.body = G.carrier) (u : Geometry.Plane) : C.supportFunction u = G.supportFunction u

Agreement with the geometry support function. Whenever a subbody shares its carrier with a solid geometry body, the two support functions coincide (both are the sSup of ⟪·, u⟫ over the common carrier). This certifies that ConvexSubbody.supportFunction is the standard support function, extended to possibly-degenerate carriers.

noncomputable def NRR.ConvexSubbody.widthFunction {K : Geometry.ConvexBody Geometry.Plane} (C : ConvexSubbody K) (u : Geometry.Plane) : ℝ

Width function of a convex subbody: w_C(u) = h_C(u) + h_C(-u).

Equations

• C.widthFunction u = C.supportFunction u + C.supportFunction (-u)

@[simp]

theorem NRR.ConvexSubbody.widthFunction_def {K : Geometry.ConvexBody Geometry.Plane} (C : ConvexSubbody K) (u : Geometry.Plane) : C.widthFunction u = C.supportFunction u + C.supportFunction (-u)

Unfolding lemma for the subbody width function.

theorem NRR.ConvexSubbody.continuous_supportFunction_dir {K : Geometry.ConvexBody Geometry.Plane} (C : ConvexSubbody K) : Continuous fun (u : Geometry.Plane) => C.supportFunction u

Fixed-body direction continuity. For a fixed subbody, u ↦ h_C(u) is continuous. The carrier is compact, hence norm-bounded, and the support function is Lipschitz in u with that bound.

theorem NRR.ConvexSubbody.abs_supportFunction_sub_le_hausdorffDist_mul_norm {K : Geometry.ConvexBody Geometry.Plane} (C D : ConvexSubbody K) (u : Geometry.Plane) : |C.supportFunction u - D.supportFunction u| ≤ Metric.hausdorffDist ↑C.body ↑D.body * ‖u‖

Hausdorff–Lipschitz estimate for subbodies. The support functions of two subbodies differ by at most d_H(C, D) · ‖u‖. Only carrier compactness and nonemptiness are used.

theorem NRR.ConvexSubbody.continuous_supportFunction {K : Geometry.ConvexBody Geometry.Plane} : Continuous fun (z : ConvexSubbody K × Geometry.Plane) => z.1.supportFunction z.2

Joint support continuity. The map (C, u) ↦ h_C(u) is continuous on ConvexSubbody K × Plane.

theorem NRR.ConvexSubbody.supportFunctionContinuousFamily {K : Geometry.ConvexBody Geometry.Plane} : Continuous fun (z : ConvexSubbody K × Geometry.Plane) => z.1.supportFunction z.2

Support-function continuous family for ConvexSubbody K: the joint map (C, u) ↦ h_C(u) is continuous. (Since the project support function is solid-only, this is the subbody-level analogue of Geometry.ConvexBody.SupportFunctionContinuousFamily for the carrier support function.)

theorem NRR.ConvexSubbody.continuous_width {K : Geometry.ConvexBody Geometry.Plane} : Continuous fun (z : ConvexSubbody K × Geometry.Plane) => z.1.widthFunction z.2

Joint width continuity. The map (C, u) ↦ w_C(u) is continuous.

theorem NRR.ConvexSubbody.widthContinuousFamily {K : Geometry.ConvexBody Geometry.Plane} : Continuous fun (z : ConvexSubbody K × Geometry.Plane) => z.1.widthFunction z.2

Width continuous family for ConvexSubbody K: the joint map (C, u) ↦ w_C(u) is continuous.

theorem NRR.BodySpace.supportFunctionContinuousFamily {K : Geometry.ConvexBody Geometry.Plane} {A : ℝ} (hA : 0 < A) : Geometry.ConvexBody.SupportFunctionContinuousFamily fun (C : BodySpace K A) => C.toGeometryConvexBody hA

Support-function continuous family for positive lower area. When A > 0, the solid bridge toGeometryConvexBody yields a Hausdorff-continuous family of solid geometry bodies, so the geometry support function is a SupportFunctionContinuousFamily.

theorem NRR.BodySpace.widthContinuousFamily {K : Geometry.ConvexBody Geometry.Plane} {A : ℝ} (hA : 0 < A) : Geometry.ConvexBody.WidthContinuousFamily fun (C : BodySpace K A) => C.toGeometryConvexBody hA

Width continuous family for positive lower area.