Singleton Supporting Contacts Imply Strict Convexity

This states that singleton supporting contact sets imply strict convexity.

Let $E$ be a finite-dimensional real inner-product space and let $u:E\to\mathbb R$ be convex. Assume that for every $x,p\in E$, whenever

$$u(x)+\langle p,y-x\rangle\le u(y)\quad\text{for all }y,$$

any point $y$ satisfying equality must equal $x$:

$$u(y)=u(x)+\langle p,y-x\rangle\Longrightarrow y=x.$$

Then $u$ is strictly convex on $E$:

$$u(a x+b y)<a u(x)+b u(y)$$

whenever $x\ne y$, $a,b>0$, and $a+b=1$.

This is the abstract bridge from uniqueness of supporting contacts to strict convexity.

Original Lean declaration header

Within namespace FunctionalInequalities.Analysis. Shown in its original module context. Proof omitted.

theorem strictConvexOn_of_contact_eq {u : E → ℝ} (hconv : ConvexOn ℝ univ u)
    (hcontact : ∀ x p : E, (∀ y, u x + ⟪p, y - x⟫ ≤ u y) →
      ∀ y, u y = u x + ⟪p, y - x⟫ → y = x) :
    StrictConvexOn ℝ univ u

Module navigation

Module: Analysis/Convex/Caffarelli.

Supporting theorems: exists_subgradient_slope_le_inner_add.

Previous: contactSet_eq_singleton_of_exposed_of_local_bounds · Next: subgradient_mem_interior_of_strictConvexOn.

Source excerpt, lines 1110–1113 · Frozen source 408915f.

import Definitions.Def_KLSModular_FunctionalInequalities_Analysis_Convex_Caffarelli

open scoped RealInnerProductSpace
open Set
variable {E : Type*}
variable [NormedAddCommGroup E] [InnerProductSpace ℝ E]
variable [FiniteDimensional ℝ E]

theorem FunctionalInequalities.Analysis.strictConvexOn_of_contact_eq_readable {u : E → ℝ} (hconv : ConvexOn ℝ univ u)
    (hcontact : ∀ x p : E, (∀ y, u x + ⟪p, y - x⟫ ≤ u y) →
      ∀ y, u y = u x + ⟪p, y - x⟫ → y = x) :
    StrictConvexOn ℝ univ u := by sorry