Energy-Preserving Ambient Extension Of An Intrinsic Test

This theorem extends an intrinsic smooth-gradient test to the ambient space without changing its intrinsic restriction or raw energy.

Let $E$ be a finite-dimensional complete real inner-product normed space with its Borel measurable structure and second-countable topology, let $\mu$ be a probability measure on $E$, and let $g$ be a smooth-gradient test for the intrinsic measure associated with $\mu$. Then there exists an ambient smooth-gradient test $f$ such that, for every intrinsic coordinate $v$,

and

The declaration is exists_ambient_extension_readable. The equality of energies is equality of the raw test-energy values, and the construction applies without a density or second-moment assumption on $\mu$.

Original Lean declaration header

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

theorem exists_ambient_extension
    (g : Energy.SmoothGradient.Test (Probability.intrinsicMeasure μ)) :
    ∃ f : Energy.SmoothGradient.Test μ,
      (∀ v, f (Probability.reconstruct μ v) = g v) ∧
      toIntrinsicL2 μ f.toL2 = g.toL2 ∧ f.energy = g.energy

Module navigation

Module: Energy/SmoothGradient/Intrinsic/Comparison.

Definition modules: Energy/SmoothGradient/Basic, Probability/AffineSupport, Energy/SmoothGradient/Intrinsic/Basic.

Next: relaxation_eq_intrinsic_energy.

Source excerpt, lines 156–160 · Frozen source 408915f.