Exact frontier range of rounded support curves

This file proves the reverse inclusion missing from the global support-curve calculus: every frontier point of a bounded rounded support envelope is hit by the support curve. The key local fact is that an active support inequality recovers both normal and tangent coordinates of the contact point.

theorem deriv_polytopeDirectionalValue_right (z : ℂ) (theta : ℝ) : deriv (polytopeDirectionalValue z) theta = -z.re * Real.sin theta + z.im * Real.cos theta

Angular derivative of the directional value of a fixed planar point.

theorem eq_smoothSupportCurve_of_mem_closedEnvelope_of_eq {h : ℝ → ℝ} (hsmooth : ContDiff ℝ (↑⊤) h) {z : ℂ} (hz : z ∈ smoothSupportClosedEnvelope h) {theta : ℝ} (hactive : polytopeDirectionalValue z theta = h theta) : z = smoothSupportCurve h theta

If a point of a smooth support envelope activates the inequality in direction theta, then it is the corresponding support-curve point.

theorem mem_smoothSupportOpenEnvelope_of_forall_lt {h : ℝ → ℝ} (hcontinuous : Continuous h) (hperiodic : Function.Periodic h (2 * Real.pi)) {z : ℂ} (hz : ∀ (theta : ℝ), polytopeDirectionalValue z theta < h theta) : z ∈ smoothSupportOpenEnvelope h

If every support inequality is strict for a continuous periodic support function, then the point lies in the open support envelope.

theorem exists_active_direction_of_mem_frontier_smoothSupportOpenEnvelope {h : ℝ → ℝ} (hcontinuous : Continuous h) (hperiodic : Function.Periodic h (2 * Real.pi)) {z : ℂ} (hz : z ∈ frontier (smoothSupportOpenEnvelope h)) : ∃ (theta : ℝ), polytopeDirectionalValue z theta = h theta

Every frontier point of a continuous periodic support envelope activates at least one of its defining support inequalities.

theorem frontier_smoothSupportOpenEnvelope_subset_range_smoothSupportCurve {h : ℝ → ℝ} (hsmooth : ContDiff ℝ (↑⊤) h) (hperiodic : Function.Periodic h (2 * Real.pi)) : frontier (smoothSupportOpenEnvelope h) ⊆ Set.range (smoothSupportCurve h)

For a smooth periodic support function, every frontier point of its open support envelope is hit by the support curve.

theorem range_polytopeRoundedSupportCurve_eq_frontier {u : Finset ℂ} (hu : u.Nonempty) {delta rho : ℝ} (hdelta : 0 < delta) (hrho : 0 < rho) : Set.range (polytopeRoundedSupportCurve u delta rho) = frontier (smoothSupportOpenEnvelope (polytopeRoundedSupport u delta rho))

The rounded positive-curvature support curve has exactly the frontier of its open support envelope as its range.

theorem image_Ico_eq_range_of_periodic {α : Type u_1} {f : ℝ → α} {p : ℝ} (hp : Function.Periodic f p) (hp_pos : 0 < p) (a : ℝ) : f '' Set.Ico a (a + p) = Set.range f

A positive-periodic function has the same range on any half-open fundamental interval as it does on the whole real line.

theorem image_Ico_polytopeRoundedSupportCurve_eq_frontier {u : Finset ℂ} (hu : u.Nonempty) {delta rho : ℝ} (hdelta : 0 < delta) (hrho : 0 < rho) : polytopeRoundedSupportCurve u delta rho '' Set.Ico 0 (2 * Real.pi) = frontier (smoothSupportOpenEnvelope (polytopeRoundedSupport u delta rho))

The rounded support curve parametrizes its whole frontier already on the standard half-open interval [0, 2 * pi).