Conjugated noise matrices

Definition

KLSModular_FunctionalInequalities_KLS_BKL_Localization_NoiseBound

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

functional-inequalitiesklskls-conjecturekls-modularlog-concavemodule-context

For a compactly supported probability measure $\mu$ and parameter $p$ , conjugatedNoiseMatrix μ hc p i is the matrix whose $(a,b)$ entry is the third cumulant of the compact posterior at $p$ , evaluated on the whitened basis vectors $A(p)^{-1/2}e_a$ , $A(p)^{-1/2}e_b$ , and $A(p)^{-1/2}e_i$ . The definition is indexed by $i\in\mathrm{Fin}\,n$ and uses the covariance operator and its inverse square root. It is a coefficient object for the noise bound; the surrounding module documentation refers to further identities and estimates not provided by this declaration.

Original module imports

import FunctionalInequalities.KLS.BKL.Localization.Coefficients
import FunctionalInequalities.KLS.BKL.CumulantEnergy.Basic
import FunctionalInequalities.KLS.BKL.Localization.Standardization
import FunctionalInequalities.KLS.BKL.Posterior.Covariance

Original declaration excerpt

Shown in the original module context.

def conjugatedNoiseMatrix (p : Param n) (i : Fin n) : Matrix (Fin n) (Fin n) ℝ :=
  Matrix.of fun a b =>
    cumulant (compactPosterior μ hc p.1 p.2 : Measure (EuclideanSpace ℝ (Fin n))) 3
      ![inverseSqrt (cov μ hc p) (EuclideanSpace.basisFun (Fin n) ℝ a),
        inverseSqrt (cov μ hc p) (EuclideanSpace.basisFun (Fin n) ℝ b),
        inverseSqrt (cov μ hc p) (EuclideanSpace.basisFun (Fin n) ℝ i)]

Module navigation

Direct project imports: KLS/BKL/Localization/Coefficients, KLS/BKL/CumulantEnergy/Basic, KLS/BKL/Localization/Standardization, KLS/BKL/Posterior/Covariance.

Theorems in source order:

Project result: The KLS conjecture.

Original module · FunctionalInequalities.KLS.BKL.Localization.NoiseBound · Frozen source 408915f.

Definition code

import Definitions.Def_KLSModular_FunctionalInequalities_KLS_BKL_Localization_Coefficients
import Definitions.Def_KLSModular_FunctionalInequalities_KLS_BKL_CumulantEnergy_Basic
import Definitions.Def_KLSModular_FunctionalInequalities_KLS_BKL_Localization_Standardization
import Definitions.Def_KLSModular_FunctionalInequalities_KLS_BKL_Posterior_Covariance

noncomputable section
open MeasureTheory
open scoped RealInnerProductSpace
open FunctionalInequalities.Probability.Posterior FunctionalInequalities.Analysis
  FunctionalInequalities.Analysis.BakryEmery
namespace FunctionalInequalities
namespace KLS
namespace BKL
variable {n : ℕ}
namespace Localization
variable (μ : ProbabilityMeasure (EuclideanSpace ℝ (Fin n)))
  (hc : IsCompact (μ : Measure (EuclideanSpace ℝ (Fin n))).support)
/-- The conjugated noise matrices `H̃_i = A^{-1/2} H_i A^{-1/2}` of BKL (85): entries
`κ₃(μ_p)(σ e_a, σ e_b, σ e_i)` with `σ = A(p)^{-1/2}`. -/
def conjugatedNoiseMatrix (p : Param n) (i : Fin n) : Matrix (Fin n) (Fin n) ℝ :=
  Matrix.of fun a b =>
    cumulant (compactPosterior μ hc p.1 p.2 : Measure (EuclideanSpace ℝ (Fin n))) 3
      ![inverseSqrt (cov μ hc p) (EuclideanSpace.basisFun (Fin n) ℝ a),
        inverseSqrt (cov μ hc p) (EuclideanSpace.basisFun (Fin n) ℝ b),
        inverseSqrt (cov μ hc p) (EuclideanSpace.basisFun (Fin n) ℝ i)]
end Localization
end BKL
end KLS
end FunctionalInequalities

Source

Lean source: https://github.com/human-ai-mathematics/kls-lean/blob/408915f/formalization/FunctionalInequalities/KLS/BKL/Localization/NoiseBound.lean#L187-L194 (repository human-ai-mathematics/kls-lean, commit 408915f, module `FunctionalInequalities.KLS.BKL.Localization.NoiseBound`, definition bundle `KLSModular_FunctionalInequalities_KLS_BKL_Localization_NoiseBound`; the repository is private at upload time).

View graph