Smooth support functions for finite planar polytopes

The directional support function of a finite convex hull is a maximum of finitely many sinusoidal functions and is generally not smooth. Its log-sum-exp regularization is infinitely differentiable and periodic. This file records the exact one-sided bounds: it dominates every vertex support value and exceeds any common upper bound by at most delta * log(card).

These estimates are the quantitative input for constructing a smooth convex support curve around a polygon.

noncomputable def polytopeDirectionalValue (z : ℂ) (theta : ℝ) : ℝ

The real support of z in the unit direction of angle theta.

Equations

• polytopeDirectionalValue z theta = z.re * Real.cos theta + z.im * Real.sin theta

noncomputable def polytopeSoftPartition (u : Finset ℂ) (delta theta : ℝ) : ℝ

The exponential partition sum used to smooth the support function of a finite point set.

Equations

• polytopeSoftPartition u delta theta = ∑ z ∈ u, Real.exp (polytopeDirectionalValue z theta / delta)

noncomputable def polytopeSoftSupport (u : Finset ℂ) (delta theta : ℝ) : ℝ

The unnormalized log-sum-exp smoothing of the finite directional support function.

Equations

• polytopeSoftSupport u delta theta = delta * Real.log (polytopeSoftPartition u delta theta)

theorem periodic_polytopeDirectionalValue (z : ℂ) : Function.Periodic (polytopeDirectionalValue z) (2 * Real.pi)

Each vertex directional value is 2*pi-periodic.

theorem periodic_polytopeSoftPartition (u : Finset ℂ) (delta : ℝ) : Function.Periodic (polytopeSoftPartition u delta) (2 * Real.pi)

The soft partition sum is 2*pi-periodic.

theorem periodic_polytopeSoftSupport (u : Finset ℂ) (delta : ℝ) : Function.Periodic (polytopeSoftSupport u delta) (2 * Real.pi)

The soft support function is 2*pi-periodic.

theorem polytopeSoftPartition_pos {u : Finset ℂ} (hu : u.Nonempty) (delta theta : ℝ) : 0 < polytopeSoftPartition u delta theta

A nonempty finite point set has a strictly positive soft partition sum.

theorem contDiff_polytopeDirectionalValue (z : ℂ) : ContDiff ℝ (↑⊤) (polytopeDirectionalValue z)

A directional value is infinitely differentiable in its angle.

theorem contDiff_polytopeSoftPartition (u : Finset ℂ) (delta : ℝ) : ContDiff ℝ (↑⊤) (polytopeSoftPartition u delta)

The soft partition sum is infinitely differentiable in its angle.

theorem contDiff_polytopeSoftSupport {u : Finset ℂ} (hu : u.Nonempty) (delta : ℝ) : ContDiff ℝ (↑⊤) (polytopeSoftSupport u delta)

For a nonempty finite point set, the soft support function is infinitely differentiable in its angle.

theorem polytopeDirectionalValue_le_softSupport {u : Finset ℂ} {z : ℂ} (hz : z ∈ u) {delta : ℝ} (hdelta : 0 < delta) (theta : ℝ) : polytopeDirectionalValue z theta ≤ polytopeSoftSupport u delta theta

Log-sum-exp dominates each individual vertex support value.

theorem polytopeDirectionalValue_le_softSupport_of_mem_convexHull {u : Finset ℂ} {z : ℂ} (hz : z ∈ (convexHull ℝ) ↑u) {delta : ℝ} (hdelta : 0 < delta) (theta : ℝ) : polytopeDirectionalValue z theta ≤ polytopeSoftSupport u delta theta

The soft support bound extends from the vertices to their real convex hull.

theorem polytopeSoftSupport_le_of_forall_directionalValue_le {u : Finset ℂ} (hu : u.Nonempty) {delta : ℝ} (hdelta : 0 < delta) (theta M : ℝ) (hM : ∀ z ∈ u, polytopeDirectionalValue z theta ≤ M) : polytopeSoftSupport u delta theta ≤ M + delta * Real.log ↑u.card

If M bounds every vertex in one direction, log-sum-exp exceeds M by at most delta * log(card u).