BKL Taylor-criterion constant

Definition

KLSModular_FunctionalInequalities_KLS_BKL_PoissonIterate_Criterion

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

functional-inequalitiesklskls-conjecturekls-modularlog-concavemodule-context

The definition taylorCriterionConstant is the real constant $100c^2$ , where $c = 2^{20}\max(1,3)^2 = 9\cdot 2^{20}$ . Thus its value is the explicit universal constant $100\bigl(2^{20}\max(1,3)^2\bigr)^2$ used for the Taylor-coefficient criterion.

Original module imports

import FunctionalInequalities.KLS.BKL.PoissonIterate.Defect
import FunctionalInequalities.KLS.BKL.PoissonIterate.TaylorRecursion
import FunctionalInequalities.KLS.LogConcave.HeatSemigroup.ApproximateEigenfunction
import FunctionalInequalities.KLS.LogConcave.HeatSemigroup.Curvature
import FunctionalInequalities.KLS.LogConcave.Regular.Basic
import FunctionalInequalities.Analysis.DyadicSummation
import FunctionalInequalities.Analysis.Tensor.BasisChange

Original declaration excerpt

Shown in the original module context.

def taylorCriterionConstant : ℝ := 100 * (2 ^ 20 * max 1 3 ^ 2) ^ 2

Module navigation

Direct project imports: KLS/BKL/PoissonIterate/Defect, KLS/BKL/PoissonIterate/TaylorRecursion, KLS/LogConcave/HeatSemigroup/ApproximateEigenfunction, KLS/LogConcave/HeatSemigroup/Curvature, KLS/LogConcave/Regular/Basic, Analysis/DyadicSummation, Analysis/Tensor/BasisChange.

Theorems in source order:

Project result: The KLS conjecture.

Original module · FunctionalInequalities.KLS.BKL.PoissonIterate.Criterion · Frozen source 408915f.

Definition code

import Definitions.Def_KLSModular_FunctionalInequalities_KLS_BKL_PoissonIterate_Defect
import Definitions.Def_KLSModular_FunctionalInequalities_KLS_BKL_PoissonIterate_TaylorRecursion
import Definitions.Def_KLSModular_FunctionalInequalities_KLS_LogConcave_HeatSemigroup_ApproximateEigenfunction
import Definitions.Def_KLSModular_FunctionalInequalities_KLS_LogConcave_HeatSemigroup_Curvature
import Definitions.Def_KLSModular_FunctionalInequalities_KLS_LogConcave_Regular_Basic
import Definitions.Def_KLSModular_FunctionalInequalities_Analysis_DyadicSummation
import Definitions.Def_KLSModular_FunctionalInequalities_Analysis_Tensor_BasisChange

noncomputable section
open MeasureTheory Filter Topology Finset
open FunctionalInequalities.Analysis.Semigroup FunctionalInequalities.Analysis.BakryEmery
open FunctionalInequalities.Analysis.Tensor
open scoped ENNReal NNReal RealInnerProductSpace InnerProductSpace ContDiff
namespace FunctionalInequalities
namespace KLS
namespace LogConcave
namespace PoissonIterate
/-- The universal constant of BKL Theorem 3.1 obtained in the operator route: `K = 100 c²` with
`c = 2^20 max(1, 3)² = 9 · 2^20`, the constant of Lemma 3.8 (route statement `J1`) at `β = 3`. -/
def taylorCriterionConstant : ℝ := 100 * (2 ^ 20 * max 1 3 ^ 2) ^ 2
end PoissonIterate
end LogConcave
end KLS
end FunctionalInequalities

Source

Lean source: https://github.com/human-ai-mathematics/kls-lean/blob/408915f/formalization/FunctionalInequalities/KLS/BKL/PoissonIterate/Criterion.lean#L367-L369 (repository human-ai-mathematics/kls-lean, commit 408915f, module `FunctionalInequalities.KLS.BKL.PoissonIterate.Criterion`, definition bundle `KLSModular_FunctionalInequalities_KLS_BKL_PoissonIterate_Criterion`; the repository is private at upload time).

View graph