Prove2Me

Affine Subtraction Translates Subgradient Images

Proved
FunctionalInequalities.Analysis.subgradientImage_sub_inner_add_const_readable

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

functional-inequalitieskls-conjecturekls-modularkls-readablelog-concave

This identifies the effect of subtracting an affine function on subgradient images.

Let EE be a real inner-product space, let u:E→Ru:E\to\mathbb R, p∈Ep\in E, c∈Rc\in\mathbb R, and G⊆EG\subseteq E. Then, using subgradientImage,

∂(u−⟨p,⋅⟩−c)(G)={q−p:q∈∂u(G)}.\partial\bigl(u-\langle p,\cdot\rangle-c\bigr)(G)=\{q-p:q\in\partial u(G)\}.

Equivalently, the subgradient image is translated by −p-p.

This is a bookkeeping identity used to transfer volume estimates under affine normalization.

Original Lean declaration header

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

theorem subgradientImage_sub_inner_add_const (u : E → ℝ) (p : E) (c : ℝ) (G : Set E) :
    subgradientImage (fun x => u x - (⟪p, x⟫ + c)) G = (fun q => q - p) '' subgradientImage u G

Module navigation

Module: Analysis/Convex/Alexandrov.

Definition modules: Analysis/Convex/Subgradient.

Previous: volume_subgradientImage_comp_affineEquiv_symm · Next: volume_subgradientImage_eq_lintegral_of_isOpen.

Source excerpt, lines 2118–2119 · Frozen source 408915f.

Preamble
import Definitions.Def_KLSModular_FunctionalInequalities_Analysis_Convex_Alexandrov

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

theorem FunctionalInequalities.Analysis.subgradientImage_sub_inner_add_const_readable (u : E → ℝ) (p : E) (c : ℝ) (G : Set E) :
    subgradientImage (fun x => u x - (⟪p, x⟫ + c)) G = (fun q => q - p) '' subgradientImage u G := by sorry
Source
Lean source: https://github.com/human-ai-mathematics/kls-lean/blob/408915f/formalization/FunctionalInequalities/Analysis/Convex/Alexandrov.lean#L2117-L2136 (repository human-ai-mathematics/kls-lean, commit 408915f, module `FunctionalInequalities.Analysis.Convex.Alexandrov`, declaration `FunctionalInequalities.Analysis.subgradientImage_sub_inner_add_const`; the repository is private at upload time).

View graph