Volume Scaling of Transported Subgradient Images

Proved

FunctionalInequalities.Analysis.volume_subgradientImage_comp_affineEquiv_symm_readable

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

functional-inequalitieskls-conjecturekls-modularkls-readablelog-concave

This gives the volume-scaling version of affine transport for subgradient images.

Let $E$ be a finite-dimensional real inner-product space with measurable and Borel structures, let $u:E\to\mathbb R$ , let $e:E\simeq_A E$ , and let $G\subseteq E$ . Writing $T=e.linear$ , one has

\operatorname{vol}\big(\operatorname{subgradientImage}(u\circ e^{-1},e(G))\big) =\operatorname{ofReal}\!\left(|\det T|^{-1}\right)\operatorname{vol}\big(\operatorname{subgradientImage}(u,G)\big).

The volume values lie in $[0,\infty]$ (ENNReal), while the determinant factor is embedded with ofReal. The declaration is volume_subgradientImage_comp_affineEquiv_symm_readable; no finiteness of either measured set is assumed.

Original Lean declaration header

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

theorem volume_subgradientImage_comp_affineEquiv_symm [MeasurableSpace E] [BorelSpace E]
    (u : E → ℝ) (e : E ≃ᵃ[ℝ] E) (G : Set E) :
    (volume : Measure E) (subgradientImage (u ∘ e.symm) (e '' G)) =
      ENNReal.ofReal |LinearMap.det (e.linear : E →ₗ[ℝ] E)|⁻¹ *
        (volume : Measure E) (subgradientImage u G)

Module navigation

Module: Analysis/Convex/Alexandrov.

Definition modules: Analysis/Convex/Subgradient.

Supporting theorems: subgradientImage_comp_affineEquiv_symm.

Previous: subgradientImage_comp_affineEquiv_symm · Next: subgradientImage_sub_inner_add_const.

Source excerpt, lines 1859–1863 · Frozen source 408915f.

Preamble

import Definitions.Def_KLSModular_FunctionalInequalities_Analysis_Convex_Alexandrov

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

Formal statement


theorem FunctionalInequalities.Analysis.volume_subgradientImage_comp_affineEquiv_symm_readable [MeasurableSpace E] [BorelSpace E]
    (u : E → ℝ) (e : E ≃ᵃ[ℝ] E) (G : Set E) :
    (volume : Measure E) (subgradientImage (u ∘ e.symm) (e '' G)) =
      ENNReal.ofReal |LinearMap.det (e.linear : E →ₗ[ℝ] E)|⁻¹ *
        (volume : Measure 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#L1858-L1939 (repository human-ai-mathematics/kls-lean, commit 408915f, module `FunctionalInequalities.Analysis.Convex.Alexandrov`, declaration `FunctionalInequalities.Analysis.volume_subgradientImage_comp_affineEquiv_symm`; the repository is private at upload time).

View graph