Local supporting hyperplanes of convex functions are global

A local minimum of a convex function on a convex set is a global minimum (IsMinOn.of_isLocalMinOn_of_convexOn). Applied to u - ℓ for a linear functional ℓ, this says that an affine function x' ↦ u x + ℓ (x' - x) lying below a convex function u near x lies below it on the whole domain. In particular a subgradient of u relative to an open neighbourhood of x in the domain is a subgradient relative to the whole domain.

The same holds when the function touching u from below at x is only differentiable there rather than affine: if u - g has a local minimum at x relative to s and g has derivative ℓ at x within s, then x' ↦ u x + ℓ (x' - x) lies below u on all of s (ConvexOn.add_le_of_isLocalMinOn_sub). No differentiability of u is needed. This is the first-order condition used for transport costs h (x - y) with h convex but not differentiable, as in Gangbo and McCann.

References

• W. Gangbo and R. J. McCann, The geometry of optimal transportation, Acta Math. 177 (1996), 113--161.

theorem ConvexOn.add_le_of_eventually_add_le {E : Type u_1} [AddCommGroup E] [TopologicalSpace E] [Module ℝ E] [IsTopologicalAddGroup E] [ContinuousSMul ℝ E] {s : Set E} {u : E → ℝ} {x : E} (hu : ConvexOn ℝ s u) (hx : x ∈ s) (ℓ : E →ₗ[ℝ] ℝ) (h : ∀ᶠ (x' : E) in nhdsWithin x s, u x + ℓ (x' - x) ≤ u x') (x' : E) : x' ∈ s → u x + ℓ (x' - x) ≤ u x'

Local supporting hyperplanes of a convex function are global. If u is convex on s, x ∈ s, and the affine function x' ↦ u x + ℓ (x' - x) lies below u at the points of s near x, then it lies below u on all of s.

theorem ConvexOn.add_le_of_isLocalMinOn_sub {F : Type u_2} [NormedAddCommGroup F] [NormedSpace ℝ F] {s : Set F} {u g : F → ℝ} {x : F} (hu : ConvexOn ℝ s u) (hx : x ∈ s) {ℓ : F →L[ℝ] ℝ} (hg : HasFDerivWithinAt g ℓ s x) (hmin : IsLocalMinOn (fun (y : F) => u y - g y) s x) (x' : F) : x' ∈ s → u x + ℓ (x' - x) ≤ u x'

A differentiable function touching a convex function from below supports it. If u is convex on s, x ∈ s, u - g has a local minimum at x relative to s, and g has derivative ℓ at x within s, then the affine function x' ↦ u x + ℓ (x' - x) lies below u on all of s. No differentiability of u is assumed.