Convex envelopes of planar support functions

A real support function determines a closed convex set by intersecting its directional halfspaces; its interior is the corresponding open convex carrier. This file develops the elementary global envelope facts needed by the smooth support-curve construction. For rounded finite-polytope supports, the original convex hull lies in that interior with the explicit rounding margin.

noncomputable def smoothSupportDirectionalLinearMap (theta : ℝ) : ℂ →ₗ[ℝ] ℝ

The real-linear directional functional at angle theta.

Equations

• smoothSupportDirectionalLinearMap theta = Real.cos theta • ↑Complex.reCLM + Real.sin theta • ↑Complex.imCLM

@[simp]

theorem smoothSupportDirectionalLinearMap_apply (theta : ℝ) (z : ℂ) : (smoothSupportDirectionalLinearMap theta) z = polytopeDirectionalValue z theta

def smoothSupportClosedEnvelope (h : ℝ → ℝ) : Set ℂ

Closed convex envelope cut out by all directional support halfspaces.

Equations

• smoothSupportClosedEnvelope h = {z : ℂ | ∀ (theta : ℝ), polytopeDirectionalValue z theta ≤ h theta}

def smoothSupportOpenEnvelope (h : ℝ → ℝ) : Set ℂ

Open carrier associated with a support function.

Equations

• smoothSupportOpenEnvelope h = interior (smoothSupportClosedEnvelope h)

theorem smoothSupportClosedEnvelope_eq_iInter (h : ℝ → ℝ) : smoothSupportClosedEnvelope h = ⋂ (theta : ℝ), {z : ℂ | polytopeDirectionalValue z theta ≤ h theta}

The support envelope as an explicit intersection of halfspaces.

theorem continuous_polytopeDirectionalValue_left (theta : ℝ) : Continuous fun (z : ℂ) => polytopeDirectionalValue z theta

Each directional-value function is continuous in the planar point.

theorem isClosed_smoothSupportClosedEnvelope (h : ℝ → ℝ) : IsClosed (smoothSupportClosedEnvelope h)

The closed support envelope is closed.

theorem convex_smoothSupportClosedEnvelope (h : ℝ → ℝ) : Convex ℝ (smoothSupportClosedEnvelope h)

The closed support envelope is convex.

theorem isOpen_smoothSupportOpenEnvelope (h : ℝ → ℝ) : IsOpen (smoothSupportOpenEnvelope h)

The open support envelope is open.

theorem convex_smoothSupportOpenEnvelope (h : ℝ → ℝ) : Convex ℝ (smoothSupportOpenEnvelope h)

The open support envelope is convex.

theorem strictConvex_smoothSupportOpenEnvelope (h : ℝ → ℝ) : StrictConvex ℝ (smoothSupportOpenEnvelope h)

In Mathlib's open-set formulation, the open support envelope is strictly convex.

theorem polytopeDirectionalValue_le_add_dist (z w : ℂ) (theta : ℝ) : polytopeDirectionalValue w theta ≤ polytopeDirectionalValue z theta + dist w z

A unit directional functional changes by at most the ambient distance.

theorem convexHull_subset_smoothSupportOpenEnvelope_polytopeRoundedSupport {u : Finset ℂ} {delta rho : ℝ} (hdelta : 0 < delta) (hrho : 0 < rho) : (convexHull ℝ) ↑u ⊆ smoothSupportOpenEnvelope (polytopeRoundedSupport u delta rho)

The convex hull lies in the open rounded-support envelope, with rho as an explicit uniform interior margin.