Smooth planar curves from support functions

For a smooth periodic real support function h, let n(theta) be the unit normal and tau(theta) = n(theta) * I the positively oriented unit tangent. The classical support curve is

gamma(theta) = h(theta) n(theta) + h'(theta) tau(theta).

Its derivative is exactly (h + h'') tau. Thus strict positivity of the curvature radius h + h'' gives a smooth periodic regular curve, with explicit speed and outward-normal formulas. These local identities are independent of the later global argument identifying the curve with the frontier of its support envelope.

noncomputable def smoothSupportUnitNormal (theta : ℝ) : ℂ

Unit outward normal at angle theta.

Equations

• smoothSupportUnitNormal theta = circleMap 0 1 theta

noncomputable def smoothSupportUnitTangent (theta : ℝ) : ℂ

Positively oriented unit tangent at angle theta.

Equations

• smoothSupportUnitTangent theta = smoothSupportUnitNormal theta * Complex.I

noncomputable def smoothSupportCurve (h : ℝ → ℝ) (theta : ℝ) : ℂ

The planar curve represented by a differentiable support function.

Equations

• smoothSupportCurve h theta = h theta • smoothSupportUnitNormal theta + deriv h theta • smoothSupportUnitTangent theta

noncomputable def smoothSupportCurvatureRadius (h : ℝ → ℝ) (theta : ℝ) : ℝ

The radius of curvature associated with a twice differentiable support function.

Equations

• smoothSupportCurvatureRadius h theta = h theta + deriv (deriv h) theta

theorem periodic_deriv_of_periodic {f : ℝ → ℝ} {p : ℝ} (hf : Function.Periodic f p) : Function.Periodic (deriv f) p

Differentiation preserves an additive period.

theorem periodic_smoothSupportUnitNormal : Function.Periodic smoothSupportUnitNormal (2 * Real.pi)

The unit normal is 2*pi-periodic.

theorem periodic_smoothSupportUnitTangent : Function.Periodic smoothSupportUnitTangent (2 * Real.pi)

The unit tangent is 2*pi-periodic.

theorem periodic_smoothSupportCurve {h : ℝ → ℝ} (hperiodic : Function.Periodic h (2 * Real.pi)) : Function.Periodic (smoothSupportCurve h) (2 * Real.pi)

A smooth periodic support function produces a periodic support curve.

theorem contDiff_smoothSupportUnitNormal : ContDiff ℝ (↑⊤) smoothSupportUnitNormal

The unit normal is infinitely differentiable.

theorem contDiff_smoothSupportUnitTangent : ContDiff ℝ (↑⊤) smoothSupportUnitTangent

The unit tangent is infinitely differentiable.

theorem contDiff_smoothSupportCurve {h : ℝ → ℝ} (hsmooth : ContDiff ℝ (↑⊤) h) : ContDiff ℝ (↑⊤) (smoothSupportCurve h)

A smooth support function produces an infinitely differentiable support curve.

theorem deriv_smoothSupportUnitNormal (theta : ℝ) : deriv smoothSupportUnitNormal theta = smoothSupportUnitTangent theta

Exact derivative of the unit normal.

theorem deriv_smoothSupportUnitTangent (theta : ℝ) : deriv smoothSupportUnitTangent theta = -smoothSupportUnitNormal theta

Exact derivative of the unit tangent.

theorem hasDerivAt_smoothSupportUnitTangent (theta : ℝ) : HasDerivAt smoothSupportUnitTangent (-smoothSupportUnitNormal theta) theta

Derivative witness for the unit tangent.

theorem deriv_smoothSupportCurve {h : ℝ → ℝ} (hsmooth : ContDiff ℝ (↑⊤) h) (theta : ℝ) : deriv (smoothSupportCurve h) theta = smoothSupportCurvatureRadius h theta • smoothSupportUnitTangent theta

Exact velocity formula for a smooth support curve.

theorem smoothSupportCurve_regular {h : ℝ → ℝ} (hsmooth : ContDiff ℝ (↑⊤) h) (hcurv : ∀ (theta : ℝ), 0 < smoothSupportCurvatureRadius h theta) (theta : ℝ) : deriv (smoothSupportCurve h) theta ≠ 0

Positive curvature radius makes the support curve regular.

theorem norm_deriv_smoothSupportCurve {h : ℝ → ℝ} (hsmooth : ContDiff ℝ (↑⊤) h) (hcurv : ∀ (theta : ℝ), 0 < smoothSupportCurvatureRadius h theta) (theta : ℝ) : ‖deriv (smoothSupportCurve h) theta‖ = smoothSupportCurvatureRadius h theta

The speed of a positive-curvature support curve is its curvature radius.

theorem neg_I_mul_deriv_smoothSupportCurve {h : ℝ → ℝ} (hsmooth : ContDiff ℝ (↑⊤) h) (theta : ℝ) : -Complex.I * deriv (smoothSupportCurve h) theta = smoothSupportCurvatureRadius h theta • smoothSupportUnitNormal theta

Rotating the positive tangent velocity clockwise gives the outward normal scaled by the curvature radius.

theorem polytopeDirectionalValue_smoothSupportCurve_self (h : ℝ → ℝ) (theta : ℝ) : polytopeDirectionalValue (smoothSupportCurve h theta) theta = h theta

The curve point has the prescribed support value in its own normal direction.

noncomputable def polytopeRoundedSupportCurve (u : Finset ℂ) (delta rho : ℝ) : ℝ → ℂ

The support curve associated with the strictly rounded log-sum-exp support of a finite polytope.

Equations

• polytopeRoundedSupportCurve u delta rho = smoothSupportCurve (polytopeRoundedSupport u delta rho)

theorem periodic_polytopeRoundedSupportCurve (u : Finset ℂ) (delta rho : ℝ) : Function.Periodic (polytopeRoundedSupportCurve u delta rho) (2 * Real.pi)

The rounded polytope support curve is 2*pi-periodic.

theorem contDiff_polytopeRoundedSupportCurve {u : Finset ℂ} (hu : u.Nonempty) (delta rho : ℝ) : ContDiff ℝ (↑⊤) (polytopeRoundedSupportCurve u delta rho)

The rounded polytope support curve is infinitely differentiable.

theorem polytopeRoundedSupportCurve_regular {u : Finset ℂ} (hu : u.Nonempty) {delta rho : ℝ} (hdelta : 0 < delta) (hrho : 0 < rho) (theta : ℝ) : deriv (polytopeRoundedSupportCurve u delta rho) theta ≠ 0

Positive smoothing and rounding scales make the rounded polytope support curve regular.

theorem polytopeDirectionalValue_le_roundedSupportCurve_self {u : Finset ℂ} {z : ℂ} (hz : z ∈ (convexHull ℝ) ↑u) {delta rho : ℝ} (hdelta : 0 < delta) (hrho : 0 ≤ rho) (theta : ℝ) : polytopeDirectionalValue z theta ≤ polytopeDirectionalValue (polytopeRoundedSupportCurve u delta rho theta) theta

In every direction, the rounded support curve lies on a supporting line outside the entire original finite convex hull.