Second-Moment Identity for Isotropic Laws

Proved

FunctionalInequalities.KLS.Isotropic.integral_norm_sq_readable

by Lazyfill · Oct 26, 2026 · Mathlib 0df444a (Lean v4.33.1)

functional-inequalitieskls-conjecturekls-modularkls-readablelog-concave

This statement records the total second moment of an isotropic law on $\mathbb{R}^n$ .

Let $\nu$ be an isotropic probability law on $\operatorname{EuclideanSpace}(\mathbb{R},\operatorname{Fin}n)$ . Then

\int \|x\|^2\,d\nu(x)=n.

The identity holds for every natural number $n$ , including $n=0$ , and is the coordinate-sum consequence of identity covariance.

Original Lean declaration header

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

theorem Isotropic.integral_norm_sq {n : ℕ}
    {ν : ProbabilityMeasure (EuclideanSpace ℝ (Fin n))} (hiso : KLS.Isotropic ν) :
    (∫ x, ‖x‖ ^ 2 ∂(ν : Measure (EuclideanSpace ℝ (Fin n)))) = (n : ℝ)

Module navigation

Module: KLS/Isotropic.

Previous: integral_fderiv_mul_fderiv_eq_inner_of_isotropic_map.

Source excerpt, lines 199–201 · Frozen source 408915f.

Preamble

import Definitions.Def_KLSModular_FunctionalInequalities_KLS_Isotropic

open MeasureTheory
variable {E : Type*}
variable [NormedAddCommGroup E] [InnerProductSpace ℝ E] [CompleteSpace E]
variable {E : Type*}
variable [NormedAddCommGroup E] [InnerProductSpace ℝ E] [CompleteSpace E]

Formal statement


theorem FunctionalInequalities.KLS.Isotropic.integral_norm_sq_readable {n : ℕ}
    {ν : ProbabilityMeasure (EuclideanSpace ℝ (Fin n))} (hiso : KLS.Isotropic ν) :
    (∫ x, ‖x‖ ^ 2 ∂(ν : Measure (EuclideanSpace ℝ (Fin n)))) = (n : ℝ) := by sorry

Source

Lean source: https://github.com/human-ai-mathematics/kls-lean/blob/408915f/formalization/FunctionalInequalities/KLS/Isotropic.lean#L197-L221 (repository human-ai-mathematics/kls-lean, commit 408915f, module `FunctionalInequalities.KLS.Isotropic`, declaration `FunctionalInequalities.KLS.Isotropic.integral_norm_sq`; the repository is private at upload time).

View graph