Derivative of the Quadratic Minus Moreau Expression

Proved

FunctionalInequalities.Analysis.hasFDerivAt_half_sq_sub_moreau_readable

by Lazyfill · Oct 26, 2026 · Mathlib 0df444a (Lean v4.33.1)

functional-inequalitieskls-conjecturekls-modularkls-readablelog-concave

This is an auxiliary differentiability statement for a resolvent-type map.

Let $E$ be a real inner-product space, let $f:E\to\mathbb R$ and $P:E\to E$ , and assume that for all $z,y\in E$ ,

f(Pz)+\langle z-Pz,y-Pz\rangle\le f(y).

Then, at every $z\in E$ , the function

w\longmapsto \frac12\|w\|^2-\left(f(Pw)+\frac12\|Pw-w\|^2\right)

has Fréchet derivative represented by the inner product with $Pz$ :

D\!\left[\frac12\|\cdot\|^2-f(P\cdot)-\frac12\|P\cdot-\cdot\|^2\right]_z(v)=\langle Pz,v\rangle.

In Lean this derivative is expressed as HasFDerivAt with linear map innerSL ℝ (P z). The result requires no convexity hypothesis beyond the displayed subgradient inequality.

Original Lean declaration header

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

theorem hasFDerivAt_half_sq_sub_moreau
    {f : E → ℝ} {P : E → E} (hP : ∀ z y, f (P z) + ⟪z - P z, y - P z⟫ ≤ f y) (z : E) :
    HasFDerivAt (fun w => (1 / 2) * ‖w‖ ^ 2 - (f (P w) + (1 / 2) * ‖P w - w‖ ^ 2))
      (innerSL ℝ (P z)) z

Module navigation

Module: Analysis/Convex/Proximal.

Previous: lipschitzWith_proximalPoint · Next: inner_hasFDerivAt_resolvent_symm.

Source excerpt, lines 204–207 · Frozen source 408915f.

Preamble

import Definitions.Def_KLSModular_FunctionalInequalities_Analysis_Convex_Proximal

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

Formal statement


theorem FunctionalInequalities.Analysis.hasFDerivAt_half_sq_sub_moreau_readable
    {f : E → ℝ} {P : E → E} (hP : ∀ z y, f (P z) + ⟪z - P z, y - P z⟫ ≤ f y) (z : E) :
    HasFDerivAt (fun w => (1 / 2) * ‖w‖ ^ 2 - (f (P w) + (1 / 2) * ‖P w - w‖ ^ 2))
      (innerSL ℝ (P z)) z := by sorry

Source

Lean source: https://github.com/human-ai-mathematics/kls-lean/blob/408915f/formalization/FunctionalInequalities/Analysis/Convex/Proximal.lean#L202-L239 (repository human-ai-mathematics/kls-lean, commit 408915f, module `FunctionalInequalities.Analysis.Convex.Proximal`, declaration `FunctionalInequalities.Analysis.hasFDerivAt_half_sq_sub_moreau`; the repository is private at upload time).

View graph