Isotropy of a Centered and Whitened Regular Potential

This statement identifies the isotropy of the law of a specified affine transformation of a regular potential.

Let $E$ be a finite-dimensional complete real inner product space with its Borel measurable structure. Let $V:E\to\mathbb R$, $a,b\in\mathbb R$, and $h_V:$ KLS.RegularPotential V a b. Write $\mu=$ RegularPotential.law hV, $c=\int x\,d\mu(x)$, and $\Sigma_\mu=$ Covariance.operator μ. Assume:

1. $W:E\to E$ is an invertible continuous linear map and $W^*=W$.
2. For every $u,v\in E$, $\langle\Sigma_\mu(Wu),Wv\rangle=\langle u,v\rangle$.

Let $\widetilde\mu$ be the law supplied by RegularPotential.comp_affine hV W.symm c, corresponding to the potential $y\mapsto V(W^{-1}y+c)$. Then

Here KLS.Isotropic means finite second moment, zero mean, and identity centered covariance. This is a normalization result for a supplied whitening map, not an assertion of its existence or uniqueness.

Original Lean declaration header

Within namespace FunctionalInequalities.KLS.RegularPotential. Shown in its original module context. Proof omitted.

theorem isotropic_comp_affine_of_whitening (hV : KLS.RegularPotential V a b)
    (W : E ≃L[ℝ] E) (hWadj : (W : E →L[ℝ] E).adjoint = W)
    (hW : ∀ u v, inner ℝ (Covariance.operator (hV.law : Measure E) (W u)) (W v) = inner ℝ u v) :
    KLS.Isotropic (comp_affine hV W.symm
      (∫ x, x ∂(hV.law : Measure E))).law

Module navigation

Module: KLS/LogConcave/Regular/Isotropic.

Definition modules: Probability/Covariance/Basic, KLS/Isotropic, KLS/LogConcave/Regular/Basic.

Supporting theorems: convexOn_of_hessian_ge, Covariance.operator_map_continuousLinearEquiv, isBorellDensity_of_eq_tilted, memLp_id_two, RegularPotential.law_comp_affine.

Previous: covariance_pos.

Source excerpt, lines 75–79 · Frozen source 408915f.