Ambient Reconstruction After Intrinsic Coordinates

This is an identity for the ambient and intrinsic $L^2$ coordinate maps.

Let $E$ be a finite-dimensional real inner-product normed space with its Borel measurable structure and second-countable topology, and let $\mu$ be a probability measure on $E$. For every element $f$ of $L^2(\mu)$, first map $f$ to intrinsic coordinates using toIntrinsicL2, and then map it back to ambient coordinates using toAmbientL2. The result is exactly $f$:

The declaration is toAmbientL2_toIntrinsicL2_readable. No completeness assumption on $E$ is required by the declaration, and the equality is equality in the $L^2$ subtype rather than merely pointwise equality of representatives. This provides the retraction identity needed when comparing ambient and intrinsic energies.

Original Lean declaration header

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

@[simp]
theorem toAmbientL2_toIntrinsicL2 (μ : ProbabilityMeasure E)
    (f : Lp ℝ 2 (μ : Measure E)) :
    toAmbientL2 μ (toIntrinsicL2 μ f) = f

Module navigation

Module: Energy/SmoothGradient/Intrinsic/Basic.

Definition modules: Probability/AffineSupport.

Source excerpt, lines 48–51 · Frozen source 408915f.