Intrinsic-coordinate smooth-gradient energy
DefinitionKLSModular_FunctionalInequalities_Energy_SmoothGradient_Intrinsic_BasicEnergy.Euclidean.toIntrinsicL2 μ and toAmbientL2 μ are measure-preserving L² linear isometries induced by reconstruction and the intrinsic map between the ambient space and the direction space of the affine support. Energy.SmoothGradient.Intrinsic.energy μ evaluates the smooth-gradient relaxation for the intrinsic law after transporting an ambient L² class to intrinsic coordinates. The simp theorem energy_apply exposes this pullback formula. The construction removes energy in directions normal to the affine support but does not identify the result with Cheeger energy.
Original module imports
import FunctionalInequalities.Energy.SmoothGradient.Basic
import FunctionalInequalities.Probability.AffineSupport
import Mathlib.MeasureTheory.Function.LpSpace.Basic
Original declaration excerpt
Shown in the original module context.
def toIntrinsicL2 (μ : ProbabilityMeasure E) :
Lp ℝ 2 (μ : Measure E) →ₗᵢ[ℝ]
Lp ℝ 2 (Probability.intrinsicMeasure μ).toMeasure :=
Lp.compMeasurePreservingₗᵢ ℝ (Probability.reconstruct μ)
(Probability.measurePreserving_reconstruct μ)
Module navigation
Direct project imports: Energy/SmoothGradient/Basic, Probability/AffineSupport.
Theorems in source order:
Project result: The KLS conjecture.
Original module · FunctionalInequalities.Energy.SmoothGradient.Intrinsic.Basic · Frozen source 408915f.
import Definitions.Def_KLSModular_FunctionalInequalities_Energy_SmoothGradient_Basic
import Definitions.Def_KLSModular_FunctionalInequalities_Probability_AffineSupport
import Mathlib.MeasureTheory.Function.LpSpace.Basic
noncomputable section
open MeasureTheory
namespace FunctionalInequalities
namespace Energy
namespace Euclidean
universe u
variable {E : Type u} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [CompleteSpace E]
[MeasurableSpace E] [BorelSpace E] [SecondCountableTopology E]
[FiniteDimensional ℝ E]
/-- Pull an ambient `L²(μ)` function back along reconstruction from intrinsic affine coordinates.
Because reconstruction preserves the probability law, this is a real linear isometry.
-/
def toIntrinsicL2 (μ : ProbabilityMeasure E) :
Lp ℝ 2 (μ : Measure E) →ₗᵢ[ℝ]
Lp ℝ 2 (Probability.intrinsicMeasure μ).toMeasure :=
Lp.compMeasurePreservingₗᵢ ℝ (Probability.reconstruct μ)
(Probability.measurePreserving_reconstruct μ)
/-- Pull an intrinsic-coordinate `L²` function back to the original ambient probability space. -/
def toAmbientL2 (μ : ProbabilityMeasure E) :
Lp ℝ 2 (Probability.intrinsicMeasure μ).toMeasure →ₗᵢ[ℝ]
Lp ℝ 2 (μ : Measure E) :=
Lp.compMeasurePreservingₗᵢ ℝ (Probability.intrinsicMap μ)
(Probability.measurePreserving_intrinsicMap μ)
end Euclidean
end Energy
end FunctionalInequalities
namespace FunctionalInequalities
namespace Energy
namespace SmoothGradient
namespace Intrinsic
open Euclidean
universe u
variable {E : Type u} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [CompleteSpace E]
[MeasurableSpace E] [BorelSpace E] [SecondCountableTopology E]
[FiniteDimensional ℝ E]
/-- The intrinsic-affine smooth-gradient relaxation, represented on the original `L²(μ)` space.
The functional first moves an `L²(μ)` class isometrically to the direction space of the affine
support, then evaluates the smooth-gradient relaxation of the intrinsic probability law.
-/
def energy (μ : ProbabilityMeasure E) :
Functional (Lp ℝ 2 (μ : Measure E)) :=
(Energy.SmoothGradient.relaxation (Probability.intrinsicMeasure μ)).comap (toIntrinsicL2 μ)
omit [CompleteSpace E] in
/-- Unfolding the intrinsic-affine relaxation exposes the isometric pullback. -/
@[simp]
theorem energy_apply (μ : ProbabilityMeasure E)
(f : Lp ℝ 2 (μ : Measure E)) :
energy μ f =
Energy.SmoothGradient.relaxation (Probability.intrinsicMeasure μ) (toIntrinsicL2 μ f) :=
rfl
end Intrinsic
end SmoothGradient
end Energy
end FunctionalInequalities