Arbitrarily tight rounded support envelopes

The quantitative support-envelope estimate becomes an arbitrary open neighborhood estimate after choosing the smoothing and rounding scales. We record an explicit choice that remains valid even for one-point finite sets, where the logarithmic cardinality term vanishes.

theorem exists_tight_polytopeRoundedSupportEnvelope {u : Finset ℂ} (hu : u.Nonempty) {epsilon : ℝ} (hepsilon : 0 < epsilon) : ∃ (delta : ℝ) (rho : ℝ), 0 < delta ∧ 0 < rho ∧ (convexHull ℝ) ↑u ⊆ smoothSupportOpenEnvelope (polytopeRoundedSupport u delta rho) ∧ closure (smoothSupportOpenEnvelope (polytopeRoundedSupport u delta rho)) ⊆ Metric.thickening epsilon ((convexHull ℝ) ↑u)

Every nonempty finite convex hull has positive log-sum-exp smoothing and rounding scales whose open envelope contains the hull while the closure of that envelope stays in a prescribed metric thickening.

theorem exists_tight_regular_polytopeRoundedSupportCurve {u : Finset ℂ} (hu : u.Nonempty) {epsilon : ℝ} (hepsilon : 0 < epsilon) : ∃ (delta : ℝ) (rho : ℝ), 0 < delta ∧ 0 < rho ∧ (convexHull ℝ) ↑u ⊆ smoothSupportOpenEnvelope (polytopeRoundedSupport u delta rho) ∧ closure (smoothSupportOpenEnvelope (polytopeRoundedSupport u delta rho)) ⊆ Metric.thickening epsilon ((convexHull ℝ) ↑u) ∧ Function.Periodic (polytopeRoundedSupportCurve u delta rho) (2 * Real.pi) ∧ ContDiff ℝ (↑⊤) (polytopeRoundedSupportCurve u delta rho) ∧ ∀ (theta : ℝ), deriv (polytopeRoundedSupportCurve u delta rho) theta ≠ 0

The tight-envelope parameters simultaneously give a smooth, periodic, everywhere regular support curve.