Two Below-Level Contacts Coincide

This is an auxiliary contact-point uniqueness lemma.

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$ and assume

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

Let $R\in\mathbb R$, assume $\{x:u(x)\le R\}$ is compact, and suppose that every compact $Q\subseteq\{x:u(x)<R\}$ admits two-sided ENNReal volume bounds for open $G$ with $\overline G\subseteq Q$:

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

with $a>0$. If $u(x_0)<R$, $u(y)<R$, and

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

then

$$y=x_0.$$

This technical lemma is used to turn strict exposure into uniqueness of contacts below a level.

Original Lean declaration header

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

private lemma eq_of_two_contacts_below {u : E → ℝ}
    (hconv : ConvexOn ℝ univ u) {x₀ p : E}
    (hp : ∀ x, u x₀ + ⟪p, x - x₀⟫ ≤ u x) {R : ℝ}
    (hK : IsCompact {x | u x ≤ R})
    (hB : ∀ Q : Set E, IsCompact Q → Q ⊆ {x | u x < 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)
    (hxR : u x₀ < R) {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: contactSet_eq_singleton_of_exposed_of_local_bounds, exists_exposed_contact_of_lt.

Previous: subgradientImage_truncatedConjugate_eq · Next: eq_of_contact_of_sublevel_bounds.

Source excerpt, lines 1758–1769 · 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]

 lemma FunctionalInequalities.Analysis.eq_of_two_contacts_below_readable {u : E → ℝ}
    (hconv : ConvexOn ℝ univ u) {x₀ p : E}
    (hp : ∀ x, u x₀ + ⟪p, x - x₀⟫ ≤ u x) {R : ℝ}
    (hK : IsCompact {x | u x ≤ R})
    (hB : ∀ Q : Set E, IsCompact Q → Q ⊆ {x | u x < 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)
    (hxR : u x₀ < R) {y : E} (hyR : u y < R)
    (hy : u y = u x₀ + ⟪p, y - x₀⟫) : y = x₀ := by sorry