Translation of covariance-gradient tests
DefinitionKLSModular_FunctionalInequalities_Energy_CovarianceGradient_TranslationEuclidean.gradient_comp_const_add identifies the gradient of with the translated gradient, and lipschitzWith_const_add records that translation is 1-Lipschitz. CovarianceGradient.Test.translate composes a covariance-gradient test for ν₂ with to obtain a test for ν₁, assuming the translation is measure-preserving and the covariance operators are equal. The resulting statement includes the required Lipschitz, , and integrability fields but does not itself assert equality of relaxation constants.
Original module imports
import FunctionalInequalities.L2.Transport
import FunctionalInequalities.Energy.CovarianceGradient.Basic
Original declaration excerpt
Shown in the original module context. Body omitted.
def translate
(hmp : MeasurePreserving (fun x ↦ c + x) (ν₁ : Measure V) (ν₂ : Measure V))
(hcov : Covariance.operator (ν₂ : Measure V) = Covariance.operator (ν₁ : Measure V))
(g : Test ν₂) : Test ν₁
Module navigation
Direct project imports: L2/Transport, Energy/CovarianceGradient/Basic.
Theorems in source order:
Project result: The KLS conjecture.
Original module · FunctionalInequalities.Energy.CovarianceGradient.Translation · Frozen source 408915f.
import Definitions.Def_KLSModular_FunctionalInequalities_L2_Transport
import Definitions.Def_KLSModular_FunctionalInequalities_Energy_CovarianceGradient_Basic
noncomputable section
open MeasureTheory Filter Topology InnerProductSpace
namespace FunctionalInequalities
namespace Energy
open Energy.Euclidean
universe u
variable {V : Type u} [NormedAddCommGroup V] [InnerProductSpace ℝ V] [CompleteSpace V]
section Tests
namespace Euclidean
/-- The gradient of a translated function is the translated gradient. -/
theorem gradient_comp_const_add (g : V → ℝ) (c x : V) :
gradient (fun y ↦ g (c + y)) x = gradient g (c + x) := by
apply (toDual ℝ V).injective
simp only [toDual_gradient]
exact fderiv_comp_add_left c
omit [InnerProductSpace ℝ V] [CompleteSpace V] in
/-- Translations are `1`-Lipschitz. -/
theorem lipschitzWith_const_add (c : V) : LipschitzWith 1 (fun x : V ↦ c + x) :=
LipschitzWith.of_dist_le_mul fun x y ↦ by simp [dist_eq_norm]
end Euclidean
variable [MeasurableSpace V] [BorelSpace V] [SecondCountableTopology V] [FiniteDimensional ℝ V]
variable {ν₁ ν₂ : ProbabilityMeasure V} {c : V}
namespace CovarianceGradient
namespace Test
/-- Composition of a covariance test with a measure-preserving translation between two laws with
the same covariance operator. -/
def translate
(hmp : MeasurePreserving (fun x ↦ c + x) (ν₁ : Measure V) (ν₂ : Measure V))
(hcov : Covariance.operator (ν₂ : Measure V) = Covariance.operator (ν₁ : Measure V))
(g : Test ν₂) : Test ν₁ where
toFun := fun x ↦ g (c + x)
lipschitz := by
obtain ⟨K, hK⟩ := g.lipschitz
exact ⟨K * 1, hK.comp (lipschitzWith_const_add c)⟩
memLp_two := by
have := g.memLp_two
rw [← hmp.map_eq] at this
exact (memLp_map_measure_iff (hmp.map_eq ▸ g.memLp_two.1) hmp.aemeasurable).mp this
integrable := by
have hdens : density ν₁ (fun x ↦ g (c + x)) =
density ν₂ g.toFun ∘ fun x ↦ c + x := by
funext x
simp only [density, Function.comp_apply, gradient_comp_const_add, hcov]
rw [hdens]
have := g.integrable
rw [← hmp.map_eq] at this
exact (integrable_map_measure (hmp.map_eq ▸ g.integrable.1) hmp.aemeasurable).mp this
end Test
end CovarianceGradient
end Tests
end Energy
end FunctionalInequalities