Covariance Relaxation as a Weighted-Gradient Relaxation

This identifies the covariance relaxation with a sequential pre-energy relaxation.

Let $V$ be a finite-dimensional complete real inner-product space with its Borel measurable structure, let $\nu$ be a probability measure on $V$, let $m$ be an additive Haar measure, and let $B:V\to V$ be continuous linear. Assume:

1. $\nu$ is absolutely continuous with respect to $m$;
2. the frontier of the support of $\nu$ has $\nu$-measure zero;
3. for every $v\in V$,

$$\langle\operatorname{Cov}(\nu)v,v\rangle=\|Bv\|^2.$$

Then

$$\operatorname{relaxation}(\nu) = \operatorname{sequentialRelaxation}\bigl(\operatorname{PreEnergy.ofLinearPMap}(\operatorname{WeightedGradient.operator}(\nu,B))\bigr).$$

The result is the formal bridge between covariance energy and the squared-norm energy of a weighted gradient operator.

Formalization Note The equality is between extended nonnegative-valued functionals; the absolute-continuity and support-frontier hypotheses are explicit.

Original Lean declaration header

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

theorem relaxation_eq_ofLinearPMap (hac : (ν : Measure V) ≪ m)
    (hfr : (ν : Measure V) (frontier (ν : Measure V).support) = 0)
    (hB : ∀ v, inner ℝ (Covariance.operator (ν : Measure V) v) v = ‖B v‖ ^ 2) :
    relaxation ν =
      (PreEnergy.ofLinearPMap (operator ν B hac)).sequentialRelaxation

Module navigation

Module: Energy/WeightedGradient/Basic.

Definition modules: Probability/Covariance/Basic, Energy/Relaxation/LinearPMap, Energy/Form/Functional, Energy/CovarianceGradient/Basic, Energy/Relaxation/Basic.

Supporting theorems: weightedTest_iff_exists_test.

Previous: weightedTest_iff_exists_test.

Source excerpt, lines 349–353 · Frozen source 408915f.

import Definitions.Def_KLSModular_FunctionalInequalities_Energy_WeightedGradient_Basic

open MeasureTheory Filter Topology InnerProductSpace
universe u
variable {V : Type u} [NormedAddCommGroup V] [InnerProductSpace ℝ V] [CompleteSpace V]
variable [MeasurableSpace V] (ν : MeasureTheory.ProbabilityMeasure V) (B : V →L[ℝ] V)
variable [BorelSpace V] [SecondCountableTopology V] [FiniteDimensional ℝ V]
  {m : MeasureTheory.Measure V} [m.IsAddHaarMeasure]
open FunctionalInequalities.Energy.WeightedGradient

theorem FunctionalInequalities.Energy.CovarianceGradient.relaxation_eq_ofLinearPMap_readable (hac : (ν : Measure V) ≪ m)
    (hfr : (ν : Measure V) (frontier (ν : Measure V).support) = 0)
    (hB : ∀ v, inner ℝ (Covariance.operator (ν : Measure V) v) v = ‖B v‖ ^ 2) :
    relaxation ν =
      (PreEnergy.ofLinearPMap (operator ν B hac)).sequentialRelaxation := by sorry