Volume Formula for Quadratic Subgradient Images

Proved

FunctionalInequalities.Analysis.volume_subgradientImage_quadraticAt_aux_readable

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

functional-inequalitieskls-conjecturekls-modularkls-readablelog-concave

This is an auxiliary volume identity for quadratic subgradient images.

Let $A$ be a positive-definite real $n\times n$ matrix, let $x_0,b\in\operatorname{EuclideanSpace}\,\mathbb R\,(\operatorname{Fin}(n))$ , let $c\in\mathbb R$ , and let $G$ be any subset of that Euclidean space. Then the Lebesgue volume of the subgradient image of $G$ under quadraticAt is

\operatorname{vol}\bigl(\operatorname{subgradientImage}(\operatorname{quadraticAt}(A,x_0,b,c),G)\bigr) =\operatorname{ofReal}(\det A)\,\operatorname{vol}(G).

The determinant factor is represented as an ENNReal value through ENNReal.ofReal. This identity is a reusable change-of-variables formula for the affine gradient map of a positive-definite quadratic.

Original Lean declaration header

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

private lemma volume_subgradientImage_quadraticAt_aux
    {n : ℕ} {A : Matrix (Fin n) (Fin n) ℝ} (hA : A.PosDef)
    (x₀ b : EuclideanSpace ℝ (Fin n)) (c : ℝ)
    {G : Set (EuclideanSpace ℝ (Fin n))} :
    (volume : Measure (EuclideanSpace ℝ (Fin n)))
        (subgradientImage (quadraticAt A x₀ b c) G) =
      ENNReal.ofReal A.det *
        (volume : Measure (EuclideanSpace ℝ (Fin n))) G

Module navigation

Module: Analysis/Convex/Alexandrov.

Definition modules: Analysis/Convex/Subgradient.

Supporting theorems: quadraticAt_subgradient_iff.

Previous: convexOn_quadraticAt · Next: infDist_frontier_le_of_forall_inner_le.

Source excerpt, lines 1603–1610 · Frozen source 408915f.

Preamble

import Definitions.Def_KLSModular_FunctionalInequalities_Analysis_Convex_Alexandrov

open MeasureTheory Set Matrix

Formal statement

 lemma FunctionalInequalities.Analysis.volume_subgradientImage_quadraticAt_aux_readable
    {n : ℕ} {A : Matrix (Fin n) (Fin n) ℝ} (hA : A.PosDef)
    (x₀ b : EuclideanSpace ℝ (Fin n)) (c : ℝ)
    {G : Set (EuclideanSpace ℝ (Fin n))} :
    (volume : Measure (EuclideanSpace ℝ (Fin n)))
        (subgradientImage (quadraticAt A x₀ b c) G) =
      ENNReal.ofReal A.det *
        (volume : Measure (EuclideanSpace ℝ (Fin n))) G := by sorry

Source

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

View graph