Ambient–Intrinsic Relaxation Energy Equality

This theorem identifies the ambient and intrinsic smooth-gradient relaxation energies for a finite-dimensional probability measure.

Let $E$ be a finite-dimensional real inner-product space that is a normed additive commutative group, complete, equipped with a measurable structure and its Borel structure, and having a second-countable topology. Let $\mu$ be a probability measure on $E$.

The two extended-valued energies, namely SmoothGradient.relaxation μ and SmoothGradient.Intrinsic.energy μ, are equal as functionals on the common original $L^2(\mu)$ space:

The equality includes the possibility that either energy takes the value $+\infty$. It provides the ambient–intrinsic identification needed to transfer statements between the two relaxed energy constructions, without imposing a density or second-moment assumption on $\mu$.

Formalization Note The energies take values in $[0,\infty]$ and are compared as extended-valued functionals. The statement is restricted to finite-dimensional real inner-product spaces and makes no assumption that the affine support has positive dimension.

Original Lean declaration header

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

theorem relaxation_eq_intrinsic_energy :
    relaxation μ = Intrinsic.energy μ

Module navigation

Module: Energy/SmoothGradient/Intrinsic/Comparison.

Definition modules: Energy/Form/Functional, Energy/SmoothGradient/Intrinsic/Basic, Energy/SmoothGradient/Basic.

Supporting theorems: toAmbientL2_toIntrinsicL2, exists_ambient_extension.

Previous: exists_ambient_extension.

Source excerpt, lines 183–184 · Frozen source 408915f.