NRR.Geometry.ConvexBody — support-function continuity under body parameters

This module provides the body-parameter continuity API for the support function. the project established continuity of u ↦ h_K(u) in the direction variable for a fixed body K; here we package the joint continuity of

(t, u) ↦ h_{K_t}(u)

when a family of convex bodies K : α → ConvexBody E varies continuously in the parameter t, plus the closure properties (constant, translation, positive scaling) that later partition-cell / perimeter continuity arguments need.

Mathlib hyperspace / Hausdorff situation

Mathlib does have a metric-space structure on nonempty compact subsets:

• Mathlib.Topology.MetricSpace.HausdorffDistance defines EMetric.hausdorffEdist and Metric.hausdorffDist on arbitrary sets, with the standard estimates.
• Mathlib.Topology.MetricSpace.Closeds upgrades this to bona-fide EMetricSpace (TopologicalSpace.NonemptyCompacts α) (and Compacts, Closeds), and Metric.NonemptyCompacts.dist_eq states that the resulting metric dist coincides with Metric.hausdorffDist.

However this instance is an EMetricSpace on NonemptyCompacts, not a ConvexBody-level topology, and wiring a ConvexBody E → NonemptyCompacts E map plus its induced topology in just to obtain joint continuity would be a much larger hyperspace development than downstream modules require. We therefore take the two-pronged approach the design allows:

• Route A (quantitative Hausdorff bound). We prove the sharp Lipschitz-type estimate |h_K(u) − h_L(u)| ≤ d_H(K, L) · ‖u‖ (abs_supportFunction_sub_le_hausdorffDist_mul_norm), which is the bridge to any Hausdorff-metric continuity statement one might want later. It is stated with Metric.hausdorffDist on the underlying sets, the current mathlib name.

• Route B (abstract family-continuity predicate). We define SupportFunctionContinuousFamily K as joint continuity of (t, u) ↦ h_{K_t}(u) and prove the closure properties (const, translate, scalePos) together with the evaluation and unit-direction restriction lemmas. Later constructions can discharge SupportFunctionContinuousFamily directly for whatever concrete family they build.

Public API

• abs_supportFunction_sub_le_hausdorffDist_mul_norm
• SupportFunctionContinuousFamily
• supportFunction_continuous_family_eval
• SupportFunctionContinuousFamily.const
• SupportFunctionContinuousFamily.translate
• SupportFunctionContinuousFamily.scalePos
• supportFunction_continuous_family_on_unit_directions

Route A — quantitative Hausdorff estimate

theorem NRR.Geometry.ConvexBody.abs_supportFunction_sub_le_hausdorffDist_mul_norm {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] (K L : ConvexBody E) (u : E) : |K.supportFunction u - L.supportFunction u| ≤ Metric.hausdorffDist K.carrier L.carrier * ‖u‖

Route B — abstract family-continuity predicate

def NRR.Geometry.ConvexBody.SupportFunctionContinuousFamily {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] {α : Type u_2} [TopologicalSpace α] (K : α → ConvexBody E) : Prop

A family of convex bodies K : α → ConvexBody E is a support-function continuous family if the map (t, u) ↦ h_{K_t}(u) is (jointly) continuous. This is the abstraction downstream perimeter / partition-cell continuity arguments consume.

Equations

• NRR.Geometry.ConvexBody.SupportFunctionContinuousFamily K = Continuous fun (p : α × E) => (K p.1).supportFunction p.2

theorem NRR.Geometry.ConvexBody.supportFunction_continuous_family_eval {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] {α : Type u_2} [TopologicalSpace α] {K : α → ConvexBody E} (hK : SupportFunctionContinuousFamily K) : Continuous fun (p : α × E) => (K p.1).supportFunction p.2

Evaluation. Unfolding the predicate: joint continuity of (t, u) ↦ h_{K_t}(u).

theorem NRR.Geometry.ConvexBody.SupportFunctionContinuousFamily.const {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] {α : Type u_2} [TopologicalSpace α] (K : ConvexBody E) : SupportFunctionContinuousFamily fun (x : α) => K

Constant family. A constant family is a support-function continuous family, by the project's continuous_supportFunction.

theorem NRR.Geometry.ConvexBody.SupportFunctionContinuousFamily.translate {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] {α : Type u_2} [TopologicalSpace α] {K : α → ConvexBody E} (hK : SupportFunctionContinuousFamily K) (a : α → E) (ha : Continuous a) : SupportFunctionContinuousFamily fun (t : α) => (K t).translate (a t)

Translated family. Translating a continuous family by a continuous vector field keeps it a support-function continuous family, using h_{K + a}(u) = ⟪a, u⟫ + h_K(u).

theorem NRR.Geometry.ConvexBody.SupportFunctionContinuousFamily.scalePos {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] {α : Type u_2} [TopologicalSpace α] {K : α → ConvexBody E} (hK : SupportFunctionContinuousFamily K) (r : α → ℝ) (hr : ∀ (t : α), 0 < r t) (hcont : Continuous r) : SupportFunctionContinuousFamily fun (t : α) => (K t).scalePos (r t) ⋯

Positively scaled family. Scaling a continuous family by a continuous positive function keeps it a support-function continuous family, using h_{r K}(u) = r · h_K(u).

theorem NRR.Geometry.ConvexBody.supportFunction_continuous_family_on_unit_directions {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] {α : Type u_2} [TopologicalSpace α] {K : α → ConvexBody E} (hK : SupportFunctionContinuousFamily K) : Continuous fun (p : α × ↑(Metric.sphere 0 1)) => (K p.1).supportFunction ↑p.2

Restriction to unit directions. The joint map restricted to the unit sphere Metric.sphere 0 1 is continuous. (the library has no bespoke sphere type; the ambient unit sphere is used.)