Subgradient image of a set

Definition

KLSModular_FunctionalInequalities_Analysis_Convex_Subgradient

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

functional-inequalitiesklskls-conjecturekls-modularlog-concavemodule-context

For $u:E\to\mathbb{R}$ on a real inner-product space and $S\subset E$ , subgradientImage u S is the set of all $p\in E$ for which there exists $x\in S$ such that $u(x)+\langle p,y-x\rangle\le u(y)$ for every $y\in E$ . Thus it is the image, over $S$ , of the pointwise subdifferential; the module also contains differentiability, gradient-image, and injectivity auxiliary results for convex functions.

Original module imports

import Mathlib.Analysis.Convex.Deriv
import Mathlib.Analysis.Calculus.Gradient.Basic
import Mathlib.Analysis.Calculus.FDeriv.Symmetric
import Mathlib.Analysis.Normed.Module.FiniteDimension
import Mathlib.Analysis.Calculus.Rademacher
import Mathlib.Analysis.Convex.Continuous
import Mathlib.Analysis.Convex.Measure
import Mathlib.Analysis.InnerProductSpace.Dual
import FunctionalInequalities.Analysis.Convex.LegendreVariation.Attainment

Original declaration excerpt

Shown in the original module context.

def subgradientImage {E : Type*} [NormedAddCommGroup E] [InnerProductSpace ℝ E] (u : E → ℝ)
    (S : Set E) : Set E :=
  {p | ∃ x ∈ S, ∀ y, u x + ⟪p, y - x⟫ ≤ u y}

Module navigation

Direct project imports: Analysis/Convex/LegendreVariation/Attainment.

Theorems in source order:

Project result: The KLS conjecture.

Original module · FunctionalInequalities.Analysis.Convex.Subgradient · Frozen source 408915f.

Definition code

import Mathlib.Analysis.Convex.Deriv
import Mathlib.Analysis.Calculus.Gradient.Basic
import Mathlib.Analysis.Calculus.FDeriv.Symmetric
import Mathlib.Analysis.Normed.Module.FiniteDimension
import Mathlib.Analysis.Calculus.Rademacher
import Mathlib.Analysis.Convex.Continuous
import Mathlib.Analysis.Convex.Measure
import Mathlib.Analysis.InnerProductSpace.Dual
import Definitions.Def_KLSModular_FunctionalInequalities_Analysis_Convex_LegendreVariation_Attainment

noncomputable section
open MeasureTheory Set
open scoped RealInnerProductSpace
section LT12ASubgradientImageMonotone
open Set
open scoped RealInnerProductSpace
open scoped Topology
namespace FunctionalInequalities
namespace Analysis
section InnerProduct
variable {E : Type*}
variable [NormedAddCommGroup E] [InnerProductSpace ℝ E]
/-- The **subgradient image** `∂u(S) = {p | ∃ x ∈ S, p is a subgradient of u at x}` (weak Letwin
route, routes/letwin-weak-definitions.md item 2). -/
def subgradientImage {E : Type*} [NormedAddCommGroup E] [InnerProductSpace ℝ E] (u : E → ℝ)
    (S : Set E) : Set E :=
  {p | ∃ x ∈ S, ∀ y, u x + ⟪p, y - x⟫ ≤ u y}
end InnerProduct
end Analysis
end FunctionalInequalities
end LT12ASubgradientImageMonotone

Source

Lean source: https://github.com/human-ai-mathematics/kls-lean/blob/408915f/formalization/FunctionalInequalities/Analysis/Convex/Subgradient.lean#L983-L987 (repository human-ai-mathematics/kls-lean, commit 408915f, module `FunctionalInequalities.Analysis.Convex.Subgradient`, definition bundle `KLSModular_FunctionalInequalities_Analysis_Convex_Subgradient`; the repository is private at upload time).

View graph