Truncated Conjugate Subgradient Identifies Maximizer

This is an auxiliary uniqueness statement for truncated conjugate maximizers.

Let $E$ be a finite-dimensional real inner-product space, let $u:E\to\mathbb R$ be continuous and strictly convex, and let $M\ge0$. Let $p,x,g\in E$ satisfy:

1. $\|x\|<M$.
2. $p$ is a subgradient of $u$ at $x$.
3. The truncated conjugate satisfies

$$u_M^*(p)=\langle p,x\rangle-u(x).$$

4. $g$ is a subgradient of the truncated conjugate at $p$:

$$u_M^*(p)+\langle g,q-p\rangle\le u_M^*(q)\quad\text{for all }q.$$

Then

$$g=x.$$

The lemma is used in the identification of the subgradient image of the truncated conjugate.

Original Lean declaration header

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

private lemma n7_subgradient_eq_maximizer {u : E → ℝ}
    (hu : Continuous u) (hstrict : StrictConvexOn ℝ univ u)
    {M : ℝ} (hM : 0 ≤ M) {p x g : E} (hx : ‖x‖ < M)
    (hp : ∀ y, u x + ⟪p, y - x⟫ ≤ u y)
    (heq : truncatedConjugate u M p = ⟪p, x⟫ - u x)
    (hg : ∀ q, truncatedConjugate u M p + ⟪g, q - p⟫ ≤ truncatedConjugate u M q) :
    g = x

Module navigation

Module: Analysis/Convex/Caffarelli.

Supporting theorems: convexOn_truncatedConjugate, exists_truncatedConjugate_eq.

Previous: isOpen_setOf_truncatedConjugate_maximizer_lt · Next: subgradientImage_truncatedConjugate_eq.

Source excerpt, lines 1598–1604 · Frozen source 408915f.

import Definitions.Def_KLSModular_FunctionalInequalities_Analysis_Convex_Caffarelli

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

 lemma FunctionalInequalities.Analysis.n7_subgradient_eq_maximizer_readable {u : E → ℝ}
    (hu : Continuous u) (hstrict : StrictConvexOn ℝ univ u)
    {M : ℝ} (hM : 0 ≤ M) {p x g : E} (hx : ‖x‖ < M)
    (hp : ∀ y, u x + ⟪p, y - x⟫ ≤ u y)
    (heq : truncatedConjugate u M p = ⟪p, x⟫ - u x)
    (hg : ∀ q, truncatedConjugate u M p + ⟪g, q - p⟫ ≤ truncatedConjugate u M q) :
    g = x := by sorry