Quantitative approximation by smooth support envelopes

For a nonempty finite point set, the rounded log-sum-exp support envelope is not only an outer neighborhood of its convex hull: it lies in the closed metric thickening whose radius is the uniform log-sum-exp overshoot. The proof uses the nearest-point characterization for closed convex sets and the direction of the displacement from a nearest point.

theorem polytopeDirectionalValue_sub_at_arg {z w : ℂ} (hzw : z ≠ w) : polytopeDirectionalValue z (z - w).arg - polytopeDirectionalValue w (z - w).arg = ‖z - w‖

Looking in the direction of a nonzero displacement recovers its norm.

theorem real_inner_eq_norm_mul_polytopeDirectionalValue_sub_at_arg (z v w : ℂ) : inner ℝ (z - v) (w - v) = ‖z - v‖ * (polytopeDirectionalValue w (z - v).arg - polytopeDirectionalValue v (z - v).arg)

The real inner product with a displacement is its norm times the directional-value difference in the displacement direction.

theorem smoothSupportClosedEnvelope_polytopeRoundedSupport_subset_cthickening {u : Finset ℂ} (hu : u.Nonempty) {delta rho : ℝ} (hdelta : 0 < delta) (hrho : 0 ≤ rho) : smoothSupportClosedEnvelope (polytopeRoundedSupport u delta rho) ⊆ Metric.cthickening (delta * Real.log ↑u.card + rho) ((convexHull ℝ) ↑u)

The rounded support envelope lies in the closed thickening of the finite convex hull by the exact uniform support overshoot.

theorem isCompact_smoothSupportClosedEnvelope_polytopeRoundedSupport {u : Finset ℂ} (hu : u.Nonempty) {delta rho : ℝ} (hdelta : 0 < delta) (hrho : 0 ≤ rho) : IsCompact (smoothSupportClosedEnvelope (polytopeRoundedSupport u delta rho))

The rounded support envelope of a nonempty finite point set is compact.

theorem isBounded_smoothSupportOpenEnvelope_polytopeRoundedSupport {u : Finset ℂ} (hu : u.Nonempty) {delta rho : ℝ} (hdelta : 0 < delta) (hrho : 0 ≤ rho) : Bornology.IsBounded (smoothSupportOpenEnvelope (polytopeRoundedSupport u delta rho))

The open rounded-support carrier is bounded.

theorem nonempty_smoothSupportOpenEnvelope_polytopeRoundedSupport {u : Finset ℂ} (hu : u.Nonempty) {delta rho : ℝ} (hdelta : 0 < delta) (hrho : 0 < rho) : (smoothSupportOpenEnvelope (polytopeRoundedSupport u delta rho)).Nonempty

Positive rounding makes the open support envelope nonempty.

theorem closure_smoothSupportOpenEnvelope_polytopeRoundedSupport {u : Finset ℂ} (hu : u.Nonempty) {delta rho : ℝ} (hdelta : 0 < delta) (hrho : 0 < rho) : closure (smoothSupportOpenEnvelope (polytopeRoundedSupport u delta rho)) = smoothSupportClosedEnvelope (polytopeRoundedSupport u delta rho)

For positive rounding, the closed support envelope is exactly the closure of its open carrier.

theorem closure_smoothSupportOpenEnvelope_polytopeRoundedSupport_subset_cthickening {u : Finset ℂ} (hu : u.Nonempty) {delta rho : ℝ} (hdelta : 0 < delta) (hrho : 0 < rho) : closure (smoothSupportOpenEnvelope (polytopeRoundedSupport u delta rho)) ⊆ Metric.cthickening (delta * Real.log ↑u.card + rho) ((convexHull ℝ) ↑u)

The closure of the open rounded-support carrier obeys the same explicit outer thickening bound.