Translation Invariance of Covariance Relaxation
ProvedFunctionalInequalities.Energy.CovarianceGradient.relaxation_translateLaw_readableThis proves translation invariance of the covariance relaxation.
Let be a complete real inner-product space with its Borel measurable structure, let be a probability measure on , let , and let , where . Then
where is the pullback isometry represented by L2.Translation.pullbackEquiv ν c.
The result formalizes independence of the covariance relaxation from the choice of affine origin.
Formalization Note No finite-dimensionality or second-countability assumption is required by the declaration.
Original Lean declaration header
Within namespace FunctionalInequalities.Energy.CovarianceGradient. Shown in its original module context. Proof omitted.
theorem relaxation_translateLaw (f : Lp ℝ 2 (Probability.translateLaw ν c : Measure V)) :
relaxation (Probability.translateLaw ν c) f = relaxation ν (L2.Translation.pullbackEquiv ν c f)
Module navigation
Module: Energy/CovarianceGradient/Translation.
Definition modules: Energy/Form/Functional, L2/Transport, Energy/CovarianceGradient/Basic, Probability/Transport.
Source excerpt, lines 128–129 · Frozen source 408915f.
import Definitions.Def_KLSModular_FunctionalInequalities_Energy_CovarianceGradient_Translation
open MeasureTheory Filter Topology InnerProductSpace
universe u
variable {V : Type u} [NormedAddCommGroup V] [InnerProductSpace ℝ V] [CompleteSpace V]
variable [MeasurableSpace V] [BorelSpace V] [SecondCountableTopology V] [FiniteDimensional ℝ V]
variable (ν : MeasureTheory.ProbabilityMeasure V) (c : V)
omit [SecondCountableTopology V] [FiniteDimensional ℝ V]
theorem FunctionalInequalities.Energy.CovarianceGradient.relaxation_translateLaw_readable (f : Lp ℝ 2 (Probability.translateLaw ν c : Measure V)) :
relaxation (Probability.translateLaw ν c) f = relaxation ν (L2.Translation.pullbackEquiv ν c f) := by sorry