Subgradient Image Integral Identity

This is the Alexandrov identity in push-forward form.

Let $E$ be a finite-dimensional real inner-product space with its Borel measurable structure. Let $u:E\to\mathbb R$ be Lipschitz and convex. Let $\nu,\mu$ be measures such that:

1. $\nu\ll\operatorname{vol}$.
2. The push-forward of $\nu$ by gradient equals $\mu$:

$$\nu\mathbin{\#}\nabla u=\mu.$$

3. $\mu\ll\operatorname{vol}$.
4. $S\subseteq E$ is compact.
5. $g:E\to[0,\infty]$ is measurable.

Then, with subgradientImage denoting $\partial u(S)$,

$$\int_{\partial u(S)} g(p)\,d\mu(p)=\int_S g(\nabla u(x))\,d\nu(x).$$

The identity is a reusable change-of-variables formula; both sides are ENNReal lower integrals.

Original Lean declaration header

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

theorem lintegral_subgradientImage_eq_of_map_gradient [FiniteDimensional ℝ E] [MeasurableSpace E] [BorelSpace E]
    {u : E → ℝ} {L : NNReal} (hu : LipschitzWith L u) (hconv : ConvexOn ℝ univ u)
    {ν μ : Measure E} (hν : ν ≪ (volume : Measure E)) (hmap : ν.map (gradient u) = μ)
    (hac : μ ≪ (volume : Measure E))
    {S : Set E} (hS : IsCompact S) (g : E → ℝ≥0∞) (hg : Measurable g) :
    ∫⁻ p in subgradientImage u S, g p ∂μ = ∫⁻ x in S, g (gradient u x) ∂ν

Module navigation

Module: Analysis/Convex/Alexandrov.

Definition modules: Analysis/Convex/Subgradient.

Supporting theorems: volume_subgradient_two_points_eq_zero.

Next: mem_subgradientImage_of_affine_le_of_nonneg_frontier.

Source excerpt, lines 78–83 · Frozen source 408915f.

import Definitions.Def_KLSModular_FunctionalInequalities_Analysis_Convex_Alexandrov

open MeasureTheory Set
open scoped RealInnerProductSpace ENNReal
variable {E : Type*}
variable [NormedAddCommGroup E] [InnerProductSpace ℝ E]

theorem FunctionalInequalities.Analysis.lintegral_subgradientImage_eq_of_map_gradient_readable [FiniteDimensional ℝ E] [MeasurableSpace E] [BorelSpace E]
    {u : E → ℝ} {L : NNReal} (hu : LipschitzWith L u) (hconv : ConvexOn ℝ univ u)
    {ν μ : Measure E} (hν : ν ≪ (volume : Measure E)) (hmap : ν.map (gradient u) = μ)
    (hac : μ ≪ (volume : Measure E))
    {S : Set E} (hS : IsCompact S) (g : E → ℝ≥0∞) (hg : Measurable g) :
    ∫⁻ p in subgradientImage u S, g p ∂μ = ∫⁻ x in S, g (gradient u x) ∂ν := by sorry