Subgradient Expansion at an Invertibly Differentiable Resolvent

This is an auxiliary local inverse-resolvent statement for convex subgradients.

Let $E$ be a real inner-product space, let $f:E\to\mathbb R$ and $P:E\to E$, and assume

Fix $z\in E$ and let $T:E\to E$ be a continuous linear equivalence such that $P$ is Fréchet differentiable at $z$ with derivative $T$. Then:

1. The only subgradient of $f$ at $Pz$ is $z-Pz$.
2. For every $\varepsilon>0$, for all $y$ sufficiently near $Pz$, every subgradient $q$ of $f$ at $y$ satisfies

The declaration subgradient_expansion_of_hasFDerivAt_resolvent_readable is a local quantitative description of the subdifferential near the image point of an invertibly differentiable resolvent.

Original Lean declaration header

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

theorem subgradient_expansion_of_hasFDerivAt_resolvent {f : E → ℝ} {P : E → E}
    (hP : ∀ z y, f (P z) + ⟪z - P z, y - P z⟫ ≤ f y) {z : E} {T : E ≃L[ℝ] E}
    (hT : HasFDerivAt P (T : E →L[ℝ] E) z) :
    (∀ q : E, (∀ y, f (P z) + ⟪q, y - P z⟫ ≤ f y) → q = z - P z) ∧
    ∀ ε > 0, ∀ᶠ y in 𝓝 (P z), ∀ q : E, (∀ w, f y + ⟪q, w - y⟫ ≤ f w) →
      ‖q - (z - P z) - (T.symm (y - P z) - (y - P z))‖ ≤ ε * ‖y - P z‖

Module navigation

Module: Analysis/Convex/SecondOrder.

Supporting theorems: resolvent_preimage_near.

Previous: resolvent_preimage_near · Next: tendsto_integral_secondDifference_mul.

Source excerpt, lines 153–158 · Frozen source 408915f.