Symmetry and Firm Nonexpansiveness of the Resolvent Derivative
ProvedFunctionalInequalities.Analysis.inner_hasFDerivAt_resolvent_symm_readableThis statement records structural properties of a differentiable resolvent.
Let be a real inner-product space, let and , and assume
Fix and suppose that has Fréchet derivative at . Then, for every ,
The declaration inner_hasFDerivAt_resolvent_symm_readable provides symmetry and the firmly nonexpansive quadratic inequality for the derivative at a single point. It is a local linear-algebraic property and does not assert global differentiability of .
Original Lean declaration header
Within namespace FunctionalInequalities.Analysis. Shown in its original module context. Proof omitted.
theorem inner_hasFDerivAt_resolvent_symm
{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 z) (v w : E) :
⟪T v, w⟫ = ⟪v, T w⟫ ∧ ‖T v‖ ^ 2 ≤ ⟪T v, v⟫
Module navigation
Module: Analysis/Convex/Proximal.
Supporting theorems: hasFDerivAt_half_sq_sub_moreau.
Previous: hasFDerivAt_half_sq_sub_moreau.
Source excerpt, lines 244–247 · Frozen source 408915f.
import Definitions.Def_KLSModular_FunctionalInequalities_Analysis_Convex_Proximal
open scoped RealInnerProductSpace Topology
variable {E : Type*}
variable [NormedAddCommGroup E] [InnerProductSpace ℝ E]
theorem FunctionalInequalities.Analysis.inner_hasFDerivAt_resolvent_symm_readable
{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 z) (v w : E) :
⟪T v, w⟫ = ⟪v, T w⟫ ∧ ‖T v‖ ^ 2 ≤ ⟪T v, v⟫ := by sorry