Open-Set Alexandrov Volume Formula

This is the Alexandrov volume identity for open sets in the moment-map setting.

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, and assume

$$\int_E e^{-u(x)}\,d\operatorname{vol}(x)=1.$$

Let $K\subseteq E$ be closed and convex, let $V:E\to\mathbb R$ be measurable, and suppose the push-forward of the tilted volume measure by $\nabla u$ equals the measure with density

$$1_K(p)\,\operatorname{ofReal}(e^{-V(p)}).$$

Then every open set $G\subseteq E$ satisfies

$$\operatorname{vol}(\partial u(G)) =\int_G \operatorname{ofReal}\!\left(e^{-u(x)+V(\nabla u(x))}\right)\,d\operatorname{vol}(x).$$

This formula is a central measure identity for the moment potential and is used to derive local Monge–Ampère bounds.

Original Lean declaration header

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

theorem volume_subgradientImage_eq_lintegral_of_isOpen [FiniteDimensional ℝ E] [MeasurableSpace E] [BorelSpace E]
    {u : E → ℝ} {L : NNReal} (hu : LipschitzWith L u) (hconv : ConvexOn ℝ univ u)
    (hnorm : ∫ x, Real.exp (-u x) ∂(volume : Measure E) = 1)
    {K : Set E} (hK : IsClosed K) (hKc : Convex ℝ K) {V : E → ℝ} (hV : Measurable V)
    (hmap : ((volume : Measure E).tilted (-u)).map (gradient u) =
      (volume : Measure E).withDensity (K.indicator fun p => ENNReal.ofReal (Real.exp (-V p))))
    {G : Set E} (hG : IsOpen G) :
    (volume : Measure E) (subgradientImage u G) =
      ∫⁻ x in G, ENNReal.ofReal (Real.exp (-u x + V (gradient u x))) ∂(volume : Measure E)

Module navigation

Module: Analysis/Convex/Alexandrov.

Definition modules: Analysis/Convex/Subgradient.

Supporting theorems: lintegral_subgradientImage_eq_of_map_gradient, subgradient_mem_of_ae_gradient_mem.

Previous: subgradientImage_sub_inner_add_const · Next: exists_inverse_subgradient_volume_bounds.

Source excerpt, lines 2194–2202 · Frozen source 408915f.

import Definitions.Def_KLSModular_FunctionalInequalities_Analysis_Convex_Alexandrov

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

theorem FunctionalInequalities.Analysis.volume_subgradientImage_eq_lintegral_of_isOpen_readable [FiniteDimensional ℝ E] [MeasurableSpace E] [BorelSpace E]
    {u : E → ℝ} {L : NNReal} (hu : LipschitzWith L u) (hconv : ConvexOn ℝ univ u)
    (hnorm : ∫ x, Real.exp (-u x) ∂(volume : Measure E) = 1)
    {K : Set E} (hK : IsClosed K) (hKc : Convex ℝ K) {V : E → ℝ} (hV : Measurable V)
    (hmap : ((volume : Measure E).tilted (-u)).map (gradient u) =
      (volume : Measure E).withDensity (K.indicator fun p => ENNReal.ofReal (Real.exp (-V p))))
    {G : Set E} (hG : IsOpen G) :
    (volume : Measure E) (subgradientImage u G) =
      ∫⁻ x in G, ENNReal.ofReal (Real.exp (-u x + V (gradient u x))) ∂(volume : Measure E) := by sorry