NRR.Geometry.ConvexBody — width continuity for parameterized families

This module packages the joint continuity of the width function for a family of convex bodies K : α → ConvexBody E varying continuously in a parameter t. Concretely we introduce

WidthContinuousFamily K : Continuous fun p : α × E => widthFunction (K p.1) p.2

the width-function analogue of SupportFunctionContinuousFamily from SupportFunctionParametric.lean, and provide the standard closure properties needed by later partition-cell / perimeter continuity arguments:

• WidthContinuousFamily.of_support — a support-function continuous family is width continuous,
• WidthContinuousFamily.const — constant families,
• WidthContinuousFamily.translate — translation by an arbitrary vector field, and
• WidthContinuousFamily.scalePos — positive scaling by a continuous factor.

Design notes

Everything reduces to the width transformation identities from WidthIdentities.lean (widthFunction_translate, widthFunction_scalePos_body) and to SupportFunctionContinuousFamily from SupportFunctionParametric.lean:

• of_support writes w = h(t, u) + h(t, -u), where the second summand is the joint support map precomposed with the continuous reparameterisation (t, u) ↦ (t, -u).
• translate is immediate: width is translation invariant, so the translated family is the same function of (t, u) as the original width family (ha is not needed but is included for a uniform interface).
• scalePos uses widthFunction_scalePos_body to rewrite the family as (t, u) ↦ r t · w_{K_t}(u) and takes the product of the (continuous) scalar with the width map.

No structure internals or sSup are unfolded here.

Import policy

WidthContinuity.lean, WidthIdentities.lean and SupportFunctionParametric.lean (all transitively via Basic.lean) already pull in import Mathlib, so no extra imports are required.

def NRR.Geometry.ConvexBody.WidthContinuousFamily {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 width continuous family if the map (t, u) ↦ w_{K_t}(u) is (jointly) continuous. This is the width-function analogue of SupportFunctionContinuousFamily.

Equations

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

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

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

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

From a support-function continuous family. If (t, u) ↦ h_{K_t}(u) is jointly continuous, then so is (t, u) ↦ w_{K_t}(u) = h_{K_t}(u) + h_{K_t}(-u).

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

Constant family. A constant family is a width continuous family.

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

Translated family. Translating a width continuous family by an arbitrary vector field preserves width continuity, because width is invariant under translations.

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

Positively scaled family. Scaling a continuous family by a continuous positive function keeps it a width continuous family, using w_{rK}(u) = r · w_K(u).