Global geometry of smooth support curves

For a smooth periodic support function with positive curvature radius, every fixed directional projection of its support curve increases strictly until the matching normal angle and decreases strictly afterward. Periodicity then turns this local derivative calculation into global support-halfspace control, uniqueness of the supporting contact, and injectivity on every fundamental period.

theorem polytopeDirectionalValue_smoothSupportCurve (h : ℝ → ℝ) (theta phi : ℝ) : polytopeDirectionalValue (smoothSupportCurve h phi) theta = h phi * Real.cos (theta - phi) + deriv h phi * Real.sin (theta - phi)

The projection of the support curve onto a normal at theta, written in normal/tangent coordinates at phi.

theorem deriv_smoothSupportCurve_projection {h : ℝ → ℝ} (hsmooth : ContDiff ℝ (↑⊤) h) (theta phi : ℝ) : deriv (fun (x : ℝ) => polytopeDirectionalValue (smoothSupportCurve h x) theta) phi = smoothSupportCurvatureRadius h phi * Real.sin (theta - phi)

The derivative of a fixed directional projection is the curvature radius times the sine of the angular displacement.

theorem hasDerivAt_smoothSupportCurve_projection {h : ℝ → ℝ} (hsmooth : ContDiff ℝ (↑⊤) h) (theta phi : ℝ) : HasDerivAt (fun (x : ℝ) => polytopeDirectionalValue (smoothSupportCurve h x) theta) (smoothSupportCurvatureRadius h phi * Real.sin (theta - phi)) phi

Derivative witness for a fixed directional projection of the support curve.

theorem strictMonoOn_smoothSupportCurve_projection_left {h : ℝ → ℝ} (hsmooth : ContDiff ℝ (↑⊤) h) (hcurv : ∀ (x : ℝ), 0 < smoothSupportCurvatureRadius h x) (theta : ℝ) : StrictMonoOn (fun (x : ℝ) => polytopeDirectionalValue (smoothSupportCurve h x) theta) (Set.Icc (theta - Real.pi) theta)

Before its normal angle, a positive-curvature support curve has strictly increasing projection onto that normal.

theorem strictAntiOn_smoothSupportCurve_projection_right {h : ℝ → ℝ} (hsmooth : ContDiff ℝ (↑⊤) h) (hcurv : ∀ (x : ℝ), 0 < smoothSupportCurvatureRadius h x) (theta : ℝ) : StrictAntiOn (fun (x : ℝ) => polytopeDirectionalValue (smoothSupportCurve h x) theta) (Set.Icc theta (theta + Real.pi))

After its normal angle, a positive-curvature support curve has strictly decreasing projection onto that normal.

theorem exists_sub_int_mul_two_pi_mem_Ico (theta phi : ℝ) : ∃ (k : ℤ), phi - ↑k * (2 * Real.pi) ∈ Set.Ico (theta - Real.pi) (theta + Real.pi)

Every real angle has an integer-period translate in the half-open interval centered at any prescribed angle.

theorem polytopeDirectionalValue_smoothSupportCurve_le {h : ℝ → ℝ} (hsmooth : ContDiff ℝ (↑⊤) h) (hperiodic : Function.Periodic h (2 * Real.pi)) (hcurv : ∀ (x : ℝ), 0 < smoothSupportCurvatureRadius h x) (theta phi : ℝ) : polytopeDirectionalValue (smoothSupportCurve h phi) theta ≤ h theta

A smooth periodic positive-curvature support curve lies in every halfspace prescribed by its support function.

theorem polytopeDirectionalValue_smoothSupportCurve_eq_self_iff {h : ℝ → ℝ} (hsmooth : ContDiff ℝ (↑⊤) h) (hperiodic : Function.Periodic h (2 * Real.pi)) (hcurv : ∀ (x : ℝ), 0 < smoothSupportCurvatureRadius h x) (theta phi : ℝ) : polytopeDirectionalValue (smoothSupportCurve h phi) theta = h theta ↔ ∃ (k : ℤ), phi = theta + ↑k * (2 * Real.pi)

A directional projection reaches its support value exactly at parameters congruent to the matching normal angle modulo 2 * pi.

theorem injOn_smoothSupportCurve_Ico {h : ℝ → ℝ} (hsmooth : ContDiff ℝ (↑⊤) h) (hperiodic : Function.Periodic h (2 * Real.pi)) (hcurv : ∀ (x : ℝ), 0 < smoothSupportCurvatureRadius h x) (a : ℝ) : Set.InjOn (smoothSupportCurve h) (Set.Ico a (a + 2 * Real.pi))

A smooth periodic positive-curvature support curve is injective on every half-open fundamental period.

theorem polytopeDirectionalValue_smoothSupportUnitNormal_self (theta : ℝ) : polytopeDirectionalValue (smoothSupportUnitNormal theta) theta = 1

A unit normal has directional value one in its own direction.

theorem smoothSupportCurve_not_mem_smoothSupportOpenEnvelope (h : ℝ → ℝ) (theta : ℝ) : smoothSupportCurve h theta ∉ smoothSupportOpenEnvelope h

A support-curve point cannot lie in the interior of its prescribed closed support envelope: moving a short distance in its outward normal direction violates the active halfspace.

theorem polytopeRoundedSupportCurve_mem_smoothSupportClosedEnvelope {u : Finset ℂ} (hu : u.Nonempty) {delta rho : ℝ} (hdelta : 0 < delta) (hrho : 0 < rho) (theta : ℝ) : polytopeRoundedSupportCurve u delta rho theta ∈ smoothSupportClosedEnvelope (polytopeRoundedSupport u delta rho)

Every point of the rounded support curve belongs to its closed support envelope.

theorem polytopeRoundedSupportCurve_mem_frontier {u : Finset ℂ} (hu : u.Nonempty) {delta rho : ℝ} (hdelta : 0 < delta) (hrho : 0 < rho) (theta : ℝ) : polytopeRoundedSupportCurve u delta rho theta ∈ frontier (smoothSupportOpenEnvelope (polytopeRoundedSupport u delta rho))

Every point of the rounded support curve lies on the frontier of the open rounded support envelope.

theorem range_polytopeRoundedSupportCurve_subset_frontier {u : Finset ℂ} (hu : u.Nonempty) {delta rho : ℝ} (hdelta : 0 < delta) (hrho : 0 < rho) : Set.range (polytopeRoundedSupportCurve u delta rho) ⊆ frontier (smoothSupportOpenEnvelope (polytopeRoundedSupport u delta rho))

The range of the rounded support curve is contained in the frontier of its open support envelope.