Import context: KLS/BKL/Posterior/Regularity

Definition

KLSModular_FunctionalInequalities_KLS_BKL_Posterior_Regularity

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

functional-inequalitiesimport-contextklskls-conjecturekls-modularlog-concavemodule-context

This bundle retains the import context of the source module FunctionalInequalities.KLS.BKL.Posterior.Regularity in the modular KLS dependency graph. It adds no new mathematical declarations. Substantive statements and proofs are represented by separate theorem nodes.

Its direct project prerequisite modules are FunctionalInequalities.Probability.Posterior.CompactDomain, FunctionalInequalities.KLS.IsotropicSupport, FunctionalInequalities.Probability.Posterior.Generator, FunctionalInequalities.KLS.LogConcave.Density.ConcaveTilt, FunctionalInequalities.Analysis.Operator.InverseSqrt, FunctionalInequalities.Probability.Posterior.JointRegularity, FunctionalInequalities.Probability.Transport, FunctionalInequalities.KLS.LogConcave.Isotropic, FunctionalInequalities.Probability.IntrinsicTranslation, FunctionalInequalities.Probability.Covariance.CauchySchwarz, FunctionalInequalities.Probability.CoordinateThirdMoment, and FunctionalInequalities.KLS.BKL.Posterior.Covariance. It also directly imports the external prerequisite modules Mathlib.Probability.Moments.Covariance and Mathlib.Probability.Moments.Variance.

Original module imports

import FunctionalInequalities.Probability.Posterior.CompactDomain
import FunctionalInequalities.KLS.IsotropicSupport
import FunctionalInequalities.Probability.Posterior.Generator
import FunctionalInequalities.KLS.LogConcave.Density.ConcaveTilt
import FunctionalInequalities.Analysis.Operator.InverseSqrt
import FunctionalInequalities.Probability.Posterior.JointRegularity
import FunctionalInequalities.Probability.Transport
import FunctionalInequalities.KLS.LogConcave.Isotropic
import FunctionalInequalities.Probability.IntrinsicTranslation
import FunctionalInequalities.Probability.Covariance.CauchySchwarz
import FunctionalInequalities.Probability.CoordinateThirdMoment
import Mathlib.Probability.Moments.Covariance
import Mathlib.Probability.Moments.Variance
import FunctionalInequalities.KLS.BKL.Posterior.Covariance

Module navigation

Direct project imports: Probability/Posterior/CompactDomain, KLS/IsotropicSupport, Probability/Posterior/Generator, KLS/LogConcave/Density/ConcaveTilt, Analysis/Operator/InverseSqrt, Probability/Posterior/JointRegularity, Probability/Transport, KLS/LogConcave/Isotropic, Probability/IntrinsicTranslation, Probability/Covariance/CauchySchwarz, Probability/CoordinateThirdMoment, KLS/BKL/Posterior/Covariance.

Theorems in source order:

Isotropic.locallyLipschitz_inverseSqrt_covariance_joint

Project result: The KLS conjecture.

Original module · FunctionalInequalities.KLS.BKL.Posterior.Regularity · Frozen source 408915f.

Definition code

import Definitions.Def_KLSModular_FunctionalInequalities_Probability_Posterior_CompactDomain
import Definitions.Def_KLSModular_FunctionalInequalities_KLS_IsotropicSupport
import Definitions.Def_KLSModular_FunctionalInequalities_Probability_Posterior_Generator
import Definitions.Def_KLSModular_FunctionalInequalities_KLS_LogConcave_Density_ConcaveTilt
import Definitions.Def_KLSModular_FunctionalInequalities_Analysis_Operator_InverseSqrt
import Definitions.Def_KLSModular_FunctionalInequalities_Probability_Posterior_JointRegularity
import Definitions.Def_KLSModular_FunctionalInequalities_Probability_Transport
import Definitions.Def_KLSModular_FunctionalInequalities_KLS_LogConcave_Isotropic
import Definitions.Def_KLSModular_FunctionalInequalities_Probability_IntrinsicTranslation
import Definitions.Def_KLSModular_FunctionalInequalities_Probability_Covariance_CauchySchwarz
import Definitions.Def_KLSModular_FunctionalInequalities_Probability_CoordinateThirdMoment
import Mathlib.Probability.Moments.Covariance
import Mathlib.Probability.Moments.Variance
import Definitions.Def_KLSModular_FunctionalInequalities_KLS_BKL_Posterior_Covariance

Source

Frozen KLS source: https://github.com/human-ai-mathematics/kls-lean/blob/408915fd28eb892a7093fa5df6f6c2699e9de144/formalization/FunctionalInequalities/KLS/BKL/Posterior/Regularity.lean#L1-L97 (commit 408915fd28eb892a7093fa5df6f6c2699e9de144, module `FunctionalInequalities.KLS.BKL.Posterior.Regularity`, import-context bundle `KLSModular_FunctionalInequalities_KLS_BKL_Posterior_Regularity`). The line range identifies the complete original source module; this bundle preserves only its direct import context.

View graph