Affine Transport of Subgradient Images

Proved

FunctionalInequalities.Analysis.subgradientImage_comp_affineEquiv_symm_readable

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

functional-inequalitieskls-conjecturekls-modularkls-readablelog-concave

This establishes the affine transport law for subgradient images.

Let $E$ be a finite-dimensional real inner-product space, let $u:E\to\mathbb R$ , let $e:E\simeq_A E$ be an affine equivalence, and let $G\subseteq E$ . If $T=e.linear$ is the linear part of $e$ , then

\operatorname{subgradientImage}(u\circ e^{-1},e(G)) = \operatorname{adj}(T^{-1})\big(\operatorname{subgradientImage}(u,G)\big).

The image on the right is the set image under the adjoint of the inverse linear part. The declaration is subgradientImage_comp_affineEquiv_symm_readable; it is an exact set equality and does not involve volume or determinant factors.

Original Lean declaration header

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

theorem subgradientImage_comp_affineEquiv_symm (u : E → ℝ) (e : E ≃ᵃ[ℝ] E) (G : Set E) :
    subgradientImage (u ∘ e.symm) (e '' G) =
      (LinearMap.adjoint (e.linear.symm : E →ₗ[ℝ] E)) '' subgradientImage u G

Module navigation

Module: Analysis/Convex/Alexandrov.

Definition modules: Analysis/Convex/Subgradient.

Previous: infDist_frontier_le_of_forall_inner_le · Next: volume_subgradientImage_comp_affineEquiv_symm.

Source excerpt, lines 1774–1776 · Frozen source 408915f.

Preamble

import Definitions.Def_KLSModular_FunctionalInequalities_Analysis_Convex_Alexandrov

variable {E : Type*}
variable [NormedAddCommGroup E]
variable [InnerProductSpace ℝ E] [FiniteDimensional ℝ E]

Formal statement


theorem FunctionalInequalities.Analysis.subgradientImage_comp_affineEquiv_symm_readable (u : E → ℝ) (e : E ≃ᵃ[ℝ] E) (G : Set E) :
    subgradientImage (u ∘ e.symm) (e '' G) =
      (LinearMap.adjoint (e.linear.symm : E →ₗ[ℝ] E)) '' subgradientImage u G := by sorry

Source

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

View graph