Sublevel Contact Uniqueness

This formalizes the Caffarelli contact-set lemma below a level.

Let $E$ be a nontrivial finite-dimensional real inner-product space with its Borel measurable structure, and let $u:E\to\mathbb R$ be convex. Fix $x_0,p\in E$ with

$$u(x_0)+\langle p,y-x_0\rangle\le u(y)\quad\text{for all }y\in E.$$

Let $R\in\mathbb R$. Assume that $\{y:u(y)\le R\}$ is compact and that every compact $Q\subseteq\{y:u(y)<R\}$ admits constants $a,b\in\mathbb R$ with $a>0$ and the two-sided bounds

$$\operatorname{ofReal}(a)\,\operatorname{vol}(G)\le\operatorname{vol}(\partial u(G))\le\operatorname{ofReal}(b)\,\operatorname{vol}(G)$$

for every open $G$ with $\overline G\subseteq Q$. Then every $y$ satisfying $u(y)<R$ and

$$u(y)=u(x_0)+\langle p,y-x_0\rangle$$

coincides with $x_0$:

$$y=x_0.$$

This is a reusable localized strict-convexity criterion; compactness is required only for the closed sublevel set, not for the full contact set.

Original Lean declaration header

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

theorem eq_of_contact_of_sublevel_bounds {u : E → ℝ} (hconv : ConvexOn ℝ univ u) {x₀ p : E}
    (hp : ∀ y, u x₀ + ⟪p, y - x₀⟫ ≤ u y) {R : ℝ} (hK : IsCompact {y | u y ≤ R})
    (hB : ∀ Q : Set E, IsCompact Q → Q ⊆ {y | u y < R} → ∃ a b : ℝ, 0 < a ∧ ∀ G : Set E,
      IsOpen G → closure G ⊆ Q →
      ENNReal.ofReal a * (volume : Measure E) G ≤ (volume : Measure E) (subgradientImage u G) ∧
      (volume : Measure E) (subgradientImage u G) ≤ ENNReal.ofReal b * (volume : Measure E) G)
    {y : E} (hyR : u y < R) (hy : u y = u x₀ + ⟪p, y - x₀⟫) : y = x₀

Module navigation

Module: Analysis/Convex/Caffarelli.

Definition modules: Analysis/Convex/Subgradient.

Supporting theorems: eq_of_two_contacts_below.

Previous: eq_of_two_contacts_below · Next: strictConvexOn_of_map_gradient.

Source excerpt, lines 1918–1924 · Frozen source 408915f.

import Definitions.Def_KLSModular_FunctionalInequalities_Analysis_Convex_Caffarelli

open MeasureTheory Set Metric Filter
open scoped RealInnerProductSpace ENNReal Topology
variable {E : Type*}
variable [NormedAddCommGroup E] [InnerProductSpace ℝ E]
variable [FiniteDimensional ℝ E] [Nontrivial E] [MeasurableSpace E] [BorelSpace E]

theorem FunctionalInequalities.Analysis.eq_of_contact_of_sublevel_bounds_readable {u : E → ℝ} (hconv : ConvexOn ℝ univ u) {x₀ p : E}
    (hp : ∀ y, u x₀ + ⟪p, y - x₀⟫ ≤ u y) {R : ℝ} (hK : IsCompact {y | u y ≤ R})
    (hB : ∀ Q : Set E, IsCompact Q → Q ⊆ {y | u y < R} → ∃ a b : ℝ, 0 < a ∧ ∀ G : Set E,
      IsOpen G → closure G ⊆ Q →
      ENNReal.ofReal a * (volume : Measure E) G ≤ (volume : Measure E) (subgradientImage u G) ∧
      (volume : Measure E) (subgradientImage u G) ≤ ENNReal.ofReal b * (volume : Measure E) G)
    {y : E} (hyR : u y < R) (hy : u y = u x₀ + ⟪p, y - x₀⟫) : y = x₀ := by sorry