Kannan–Lovász–Simonovits conjecture

DefinitionOuter Minkowski boundary measure#✓fully proved

Let \(\mu\) be a measure on a pseudometric space \(E\) and let \(A \subseteq E\). For \(\varepsilon > 0\) let \(A_\varepsilon = \{x \in E : \inf_{a \in A} d(x, a) \le \varepsilon\}\) be the closed \(\varepsilon\)-neighbourhood of \(A\), with \(\inf \emptyset = \infty\). The outer Minkowski boundary measure of \(A\) with respect to \(\mu\) is

\[\mu^+(A) = \liminf_{\varepsilon \to 0^+} \frac{\mu(A_\varepsilon) - \mu(A)}{\varepsilon},\]

where the difference and the quotient are computed in \([0, \infty]\), with \(\infty - \infty = 0\).

noncomputable def outerMinkowskiBoundary {E : Type*} [PseudoMetricSpace E]
    [MeasurableSpace E] (μ : Measure E) (A : Set E) : ℝ≥0∞ :=
  Filter.liminf (fun ε : ℝ => (μ (Metric.cthickening ε A) - μ A) / ENNReal.ofReal ε)
    (nhdsWithin 0 (Set.Ioi 0))

Used by 5

Used byCheeger coefficient · The Cheeger coefficient is at most the half-space Cheeger coefficient · Cheeger coefficient of the zero measure · Half-space Cheeger coefficient · The empty set has zero outer Minkowski boundary

DefinitionCheeger coefficient#✓fully proved

For a measure \(\mu\) on a pseudometric space \(E\) equipped with a σ-algebra, the Cheeger coefficient of \(\mu\) is the infimum in \([0, \infty]\) of \(\mu^+(A) / \min(\mu(A), 1 - \mu(A))\) over all measurable sets \(A \subseteq E\) with \(0 < \mu(A) < 1\), where \(\mu^+(A) = \liminf_{\varepsilon \to 0^+} (\mu(A_\varepsilon) - \mu(A)) / \varepsilon\) is the outer Minkowski boundary measure of \(A\) and \(A_\varepsilon\) is the closed \(\varepsilon\)-neighbourhood of \(A\). The infimum of the empty family is \(\infty\); the measure \(\mu\) is not required to be a probability measure.

noncomputable def cheegerCoefficient {E : Type*} [PseudoMetricSpace E]
    [MeasurableSpace E] (μ : Measure E) : ℝ≥0∞ :=
  sInf {v | ∃ A : Set E, MeasurableSet A ∧ 0 < μ A ∧ μ A < 1 ∧
    outerMinkowskiBoundary μ A / min (μ A) (1 - μ A) = v}

Uses 1 · Used by 4

Statement usesOuter Minkowski boundary measure

Used byThe Cheeger coefficient is at most the half-space Cheeger coefficient · Cheeger coefficient of the zero measure · Inverse Cheeger constant · Inverse Cheeger constant of the zero measure

DefinitionInverse Cheeger constant#✓fully proved

For a measure \(\mu\) on a pseudometric space \(E\) equipped with a σ-algebra, the inverse Cheeger constant of \(\mu\) is \(1 / h(\mu) \in [0, \infty]\), where \(h(\mu)\) is the Cheeger coefficient of \(\mu\), with the conventions \(1 / 0 = \infty\) and \(1 / \infty = 0\).

noncomputable def inverseCheegerConstant {E : Type*} [PseudoMetricSpace E]
    [MeasurableSpace E] (μ : Measure E) : ℝ≥0∞ :=
  (cheegerCoefficient μ)⁻¹

Uses 1 · Used by 10

Statement usesCheeger coefficient

Used byLower Poincaré–Cheeger comparison with coefficient 1/π · Dimensional KLS constant · Inverse Cheeger constant bounded by the KLS constant · Inverse Cheeger constant bounded by the dimensional KLS constant · Inverse Cheeger constant of the zero measure · Lower Poincaré–Cheeger comparison with coefficient 1/9 · Bounding the KLS constant measure by measure · Finiteness of the KLS constant · Cheeger's inequality for isotropic log-concave measures · Inverse Cheeger constant of the standard Gaussian

DefinitionHalf-spaces#✓fully proved

A set \(A \subseteq \mathbb{R}^n\) is a half-space if there are a nonzero vector \(v \in \mathbb{R}^n\) and a real number \(a\) such that \(A = \{x \in \mathbb{R}^n : \langle v, x \rangle \le a\}\).

def IsHalfspace {n : ℕ} (A : Set (EuclideanSpace ℝ (Fin n))) : Prop :=
  ∃ v : EuclideanSpace ℝ (Fin n), v ≠ 0 ∧ ∃ a : ℝ, A = {x | inner ℝ v x ≤ a}

Used by 2

Used byThe Cheeger coefficient is at most the half-space Cheeger coefficient · Half-space Cheeger coefficient

DefinitionHalf-space Cheeger coefficient#✓fully proved

For a measure \(\mu\) on \(\mathbb{R}^n\) with the Euclidean metric, the half-space Cheeger coefficient of \(\mu\) is the infimum in \([0, \infty]\) of \(\mu^+(H) / \min(\mu(H), 1 - \mu(H))\) over all closed half-spaces \(H = \{x : \langle v, x \rangle \le a\}\) with \(v \ne 0\) and \(a \in \mathbb{R}\) such that \(0 < \mu(H) < 1\), where \(\mu^+(H)\) is the outer Minkowski boundary measure of \(H\). The infimum of the empty family is \(\infty\).

noncomputable def halfspaceCheegerCoefficient {n : ℕ}
    (μ : Measure (EuclideanSpace ℝ (Fin n))) : ℝ≥0∞ :=
  sInf {v | ∃ A : Set (EuclideanSpace ℝ (Fin n)),
    MeasurableSet A ∧ IsHalfspace A ∧ 0 < μ A ∧ μ A < 1 ∧
      outerMinkowskiBoundary μ A / min (μ A) (1 - μ A) = v}

Uses 2 · Used by 2

Statement usesHalf-spaces · Outer Minkowski boundary measure

Used byThe Cheeger coefficient is at most the half-space Cheeger coefficient · Inverse half-space Cheeger constant

DefinitionInverse half-space Cheeger constant#✓fully proved

For a measure \(\mu\) on \(\mathbb{R}^n\), the inverse half-space Cheeger constant of \(\mu\) is \(h^{-1}\), where \(h \in [0, \infty]\) is the half-space Cheeger coefficient of \(\mu\) and the inverse is taken in \([0, \infty]\), so that \(0^{-1} = \infty\) and \(\infty^{-1} = 0\).

noncomputable def inverseHalfspaceCheegerConstant {n : ℕ}
    (μ : Measure (EuclideanSpace ℝ (Fin n))) : ℝ≥0∞ :=
  (halfspaceCheegerCoefficient μ)⁻¹

Uses 1

Statement usesHalf-space Cheeger coefficient

DefinitionDimensional KLS constant#✓fully proved

For \(n \in \mathbb{N}\), the dimensional KLS constant in dimension \(n\) is the supremum in \([0, \infty]\) of the inverse Cheeger constants of all isotropic log-concave probability measures on \(\mathbb{R}^n\) with the Euclidean metric.

noncomputable def dimensionalKlsConstant (n : ℕ) : ℝ≥0∞ :=
  sSup {v | ∃ μ : Measure (EuclideanSpace ℝ (Fin n)),
    IsIsotropicLogConcave μ ∧ inverseCheegerConstant μ = v}

Uses 2 · Used by 14

Statement usesInverse Cheeger constant · Isotropic log-concave probability measures

Used byChen's subpolynomial bound on the KLS constant, weaker form · Dimensional KLS constants are bounded by the KLS constant · Inverse Cheeger constant bounded by the KLS constant · Inverse Cheeger constant bounded by the dimensional KLS constant · Jambulapati–Lee–Vempala polylogarithmic bound on the KLS constant · Kannan–Lovász–Simonovits bound on the KLS constant · Klartag–Lehec polylogarithmic bound on the KLS constant · Klartag's square-root-logarithmic bound on the KLS constant · KLS constant · Bounding the KLS constant dimension by dimension · Bounding the KLS constant measure by measure · Dimensional KLS constant versus thin-shell variance, up to a squared logarithm · Lee–Vempala bound on the KLS constant · Lehec's reported polylogarithmic bound on the KLS constant, weakened

DefinitionKLS constant#✓fully proved

The KLS constant is the supremum in \([0, \infty]\) of the dimensional KLS constants in dimension \(n\), taken over all positive integers \(n\).

noncomputable def klsConstant : ℝ≥0∞ :=
  sSup {v | ∃ n : ℕ, 0 < n ∧ dimensionalKlsConstant n = v}

Uses 1 · Used by 6

Statement usesDimensional KLS constant

Used byDimensional KLS constants are bounded by the KLS constant · Inverse Cheeger constant bounded by the KLS constant · Bounding the KLS constant dimension by dimension · Bounding the KLS constant measure by measure · Finiteness of the KLS constant · A lower bound for the KLS constant

DefinitionSmooth Poincaré bounds#✓fully proved

Let \(\mu\) be a measure on \(\mathbb{R}^n\) and let \(C \in [0, \infty]\). For a differentiable \(g : \mathbb{R}^n \to \mathbb{R}\) write \(\|\nabla g(x)\|\) for the Euclidean norm of the gradient of \(g\) at \(x\) (equivalently, the operator norm of the derivative of \(g\) at \(x\)). Then \(C\) is a smooth Poincaré bound for \(\mu\) if for every infinitely differentiable function \(f : \mathbb{R}^n \to \mathbb{R}\) such that \(f\), \(f^2\) and \(\|\nabla f\|^2\) are \(\mu\)-integrable,

\[\int \Big(f(x) - \int f \, d\mu\Big)^2 \, d\mu(x) \le C \int \|\nabla f(x)\|^2 \, d\mu(x),\]

where the outer integral on the left and the integral on the right are computed in \([0, \infty]\) with \(0 \cdot \infty = 0\), and the inner integral \(\int f \, d\mu\) is the usual real integral. The measure \(\mu\) need not be a probability measure.

def IsSmoothPoincareBound {n : ℕ} (μ : Measure (EuclideanSpace ℝ (Fin n)))
    (C : ℝ≥0∞) : Prop :=
  ∀ f : EuclideanSpace ℝ (Fin n) → ℝ, ContDiff ℝ ∞ f → Integrable f μ →
    Integrable (fun x => (f x) ^ 2) μ →
    Integrable (fun x => ‖fderiv ℝ f x‖ ^ 2) μ →
    (∫⁻ x, ENNReal.ofReal ((f x - ∫ y, f y ∂μ) ^ 2) ∂μ) ≤
      C * ∫⁻ x, ENNReal.ofReal (‖fderiv ℝ f x‖ ^ 2) ∂μ

Used by 3

Used bySmooth Poincaré bounds are upward closed · Smooth Poincaré constant · The smooth Poincaré constant is at most every smooth Poincaré bound

DefinitionSmooth Poincaré constant#✓fully proved

The smooth Poincaré constant of a measure \(\mu\) on \(\mathbb{R}^n\) is the infimum in \([0, \infty]\) of all \(C \in [0, \infty]\) that are smooth Poincaré bounds for \(\mu\); it is \(\infty\) when \(\mu\) has no smooth Poincaré bound.

noncomputable def smoothPoincareConstant {n : ℕ}
    (μ : Measure (EuclideanSpace ℝ (Fin n))) : ℝ≥0∞ :=
  sInf {C | IsSmoothPoincareBound μ C}

Uses 1 · Used by 4

Statement usesSmooth Poincaré bounds

Used byLower Poincaré–Cheeger comparison with coefficient 1/π · Lower Poincaré–Cheeger comparison with coefficient 1/9 · Cheeger's inequality for isotropic log-concave measures · The smooth Poincaré constant is at most every smooth Poincaré bound

TheoremThe empty set has zero outer Minkowski boundary#✓fully proved

For every measure \(\mu\) on a pseudometric space \(E\), the outer Minkowski boundary measure of the empty set with respect to \(\mu\) is \(0\).

theorem outerMinkowskiBoundary_empty {E : Type*} [PseudoMetricSpace E]
    [MeasurableSpace E] (μ : Measure E) : outerMinkowskiBoundary μ ∅ = 0

Uses 1

Statement usesOuter Minkowski boundary measure

TheoremCheeger coefficient of the zero measure#✓fully proved

On every pseudometric space \(E\) equipped with a σ-algebra, the zero measure has Cheeger coefficient \(\infty\).

No set has measure strictly between \(0\) and \(1\) under the zero measure, so the infimum is taken over the empty family.

theorem cheegerCoefficient_zero {E : Type*} [PseudoMetricSpace E] [MeasurableSpace E] :
    cheegerCoefficient (0 : Measure E) = ⊤

Uses 2 · Used by 1

Statement usesCheeger coefficient

Proof usesOuter Minkowski boundary measure

Used byInverse Cheeger constant of the zero measure

TheoremInverse Cheeger constant of the zero measure#✓fully proved

On every pseudometric space \(E\) equipped with a σ-algebra, the zero measure has inverse Cheeger constant \(0\).

theorem inverseCheegerConstant_zero {E : Type*} [PseudoMetricSpace E] [MeasurableSpace E] :
    inverseCheegerConstant (0 : Measure E) = 0

Uses 3

Statement usesInverse Cheeger constant

Proof usesCheeger coefficient · Cheeger coefficient of the zero measure

TheoremThe Cheeger coefficient is at most the half-space Cheeger coefficient#✓fully proved

For every measure \(\mu\) on \(\mathbb{R}^n\) with the Euclidean metric, the Cheeger coefficient of \(\mu\) is at most its half-space Cheeger coefficient.

theorem cheegerCoefficient_le_halfspace {n : ℕ}
    (μ : Measure (EuclideanSpace ℝ (Fin n))) :
    cheegerCoefficient μ ≤ halfspaceCheegerCoefficient μ

Uses 4

Statement usesCheeger coefficient · Half-space Cheeger coefficient

Proof usesHalf-spaces · Outer Minkowski boundary measure

TheoremInverse Cheeger constant bounded by the dimensional KLS constant#✓fully proved

For every \(n \in \mathbb{N}\) and every isotropic log-concave probability measure \(\mu\) on \(\mathbb{R}^n\) with the Euclidean metric, the inverse Cheeger constant of \(\mu\) is at most the dimensional KLS constant in dimension \(n\).

theorem inverseCheegerConstant_le_dimensional {n : ℕ}
    {μ : Measure (EuclideanSpace ℝ (Fin n))} (hμ : IsIsotropicLogConcave μ) :
    inverseCheegerConstant μ ≤ dimensionalKlsConstant n

Uses 3 · Used by 1

Statement usesDimensional KLS constant · Inverse Cheeger constant · Isotropic log-concave probability measures

Used byInverse Cheeger constant bounded by the KLS constant

TheoremDimensional KLS constants are bounded by the KLS constant#✓fully proved

For every positive integer \(n\), the dimensional KLS constant in dimension \(n\) is at most the KLS constant.

theorem dimensionalKlsConstant_le_constant {n : ℕ} (hn : 0 < n) :
    dimensionalKlsConstant n ≤ klsConstant

Uses 2 · Used by 2

Statement usesDimensional KLS constant · KLS constant

Used byInverse Cheeger constant bounded by the KLS constant · Bounding the KLS constant dimension by dimension

TheoremInverse Cheeger constant bounded by the KLS constant#✓fully proved

For every positive integer \(n\) and every isotropic log-concave probability measure \(\mu\) on \(\mathbb{R}^n\) with the Euclidean metric, the inverse Cheeger constant of \(\mu\) is at most the KLS constant.

theorem inverseCheegerConstant_le_constant {n : ℕ} (hn : 0 < n)
    {μ : Measure (EuclideanSpace ℝ (Fin n))} (hμ : IsIsotropicLogConcave μ) :
    inverseCheegerConstant μ ≤ klsConstant

Uses 6 · Used by 1

Statement usesInverse Cheeger constant · KLS constant · Isotropic log-concave probability measures

Proof usesDimensional KLS constant · Dimensional KLS constants are bounded by the KLS constant · Inverse Cheeger constant bounded by the dimensional KLS constant

Used byBounding the KLS constant measure by measure

TheoremBounding the KLS constant dimension by dimension#✓fully proved

For every \(C \in [0, \infty]\), the KLS constant is at most \(C\) if and only if, for every positive integer \(n\), the dimensional KLS constant in dimension \(n\) is at most \(C\).

theorem klsConstant_le_iff {C : ℝ≥0∞} :
    klsConstant ≤ C ↔ ∀ n : ℕ, 0 < n → dimensionalKlsConstant n ≤ C

Uses 3 · Used by 1

Statement usesDimensional KLS constant · KLS constant

Proof usesDimensional KLS constants are bounded by the KLS constant

Used byBounding the KLS constant measure by measure

TheoremBounding the KLS constant measure by measure#✓fully proved

For every \(C \in [0, \infty]\), the KLS constant is at most \(C\) if and only if, for every positive integer \(n\) and every isotropic log-concave probability measure \(\mu\) on \(\mathbb{R}^n\), the inverse Cheeger constant of \(\mu\) is at most \(C\).

theorem klsConstant_le_iff_measures {C : ℝ≥0∞} :
    klsConstant ≤ C ↔ ∀ n : ℕ, 0 < n →
      ∀ μ : Measure (EuclideanSpace ℝ (Fin n)), IsIsotropicLogConcave μ →
        inverseCheegerConstant μ ≤ C

Uses 6 · Used by 1

Statement usesInverse Cheeger constant · KLS constant · Isotropic log-concave probability measures

Proof usesDimensional KLS constant · Inverse Cheeger constant bounded by the KLS constant · Bounding the KLS constant dimension by dimension

Used byFiniteness of the KLS constant

TheoremFiniteness of the KLS constant#✓fully proved

The KLS constant is finite if and only if there is a real number \(C\) such that, for every positive integer \(n\) and every isotropic log-concave probability measure \(\mu\) on \(\mathbb{R}^n\), the inverse Cheeger constant of \(\mu\) is at most \(\max(C, 0)\).

The right-hand side is the Kannan–Lovász–Simonovits (KLS) conjecture.

theorem klsConstant_lt_top_iff : klsConstant < ⊤ ↔
    ∃ C : ℝ, ∀ n : ℕ, 0 < n →
      ∀ μ : Measure (EuclideanSpace ℝ (Fin n)), IsIsotropicLogConcave μ →
        inverseCheegerConstant μ ≤ ENNReal.ofReal C

Uses 4

Statement usesInverse Cheeger constant · KLS constant · Isotropic log-concave probability measures

Proof usesBounding the KLS constant measure by measure

TheoremSmooth Poincaré bounds are upward closed#✓fully proved

Let \(\mu\) be a measure on \(\mathbb{R}^n\) and let \(C \le D\) in \([0, \infty]\). If \(C\) is a smooth Poincaré bound for \(\mu\), then so is \(D\).

theorem IsSmoothPoincareBound.mono {n : ℕ}
    {μ : Measure (EuclideanSpace ℝ (Fin n))} {C D : ℝ≥0∞}
    (hC : IsSmoothPoincareBound μ C) (hCD : C ≤ D) : IsSmoothPoincareBound μ D

Uses 1

Statement usesSmooth Poincaré bounds

TheoremThe smooth Poincaré constant is at most every smooth Poincaré bound#✓fully proved

Let \(\mu\) be a measure on \(\mathbb{R}^n\) and let \(C \in [0, \infty]\). If \(C\) is a smooth Poincaré bound for \(\mu\), then the smooth Poincaré constant of \(\mu\) is at most \(C\).

theorem smoothPoincareConstant_le_of_bound {n : ℕ}
    {μ : Measure (EuclideanSpace ℝ (Fin n))} {C : ℝ≥0∞}
    (hC : IsSmoothPoincareBound μ C) : smoothPoincareConstant μ ≤ C

Uses 2

Statement usesSmooth Poincaré bounds · Smooth Poincaré constant

TheoremKannan–Lovász–Simonovits bound on the KLS constant#●ready to prove

There are a real \(C > 0\) and an integer \(N \ge 3\) such that for every \(n \ge N\) the dimensional KLS constant \(\psi_n \in [0, \infty]\) satisfies \(\psi_n \le C \sqrt{n}\).

public theorem_wanted kannanLovaszSimonovits1995_bound :
    ∃ C : ℝ, 0 < C ∧ ∃ N : ℕ, 3 ≤ N ∧ ∀ n : ℕ, N ≤ n →
      dimensionalKlsConstant n ≤ ENNReal.ofReal (C * Real.sqrt n)

Sources

• Kannan, Lovasz and Simonovits, DCG 13 (1995), 541--560; optimizationproblems constants/20c.md, KLS1995 row.

Uses 1

Statement usesDimensional KLS constant

TheoremLee–Vempala bound on the KLS constant#●ready to prove

There are a real \(C > 0\) and an integer \(N \ge 3\) such that for every \(n \ge N\) the dimensional KLS constant \(\psi_n \in [0, \infty]\) satisfies \(\psi_n \le C n^{1/4}\).

public theorem_wanted leeVempala2024_bound :
    ∃ C : ℝ, 0 < C ∧ ∃ N : ℕ, 3 ≤ N ∧ ∀ n : ℕ, N ≤ n →
      dimensionalKlsConstant n ≤ ENNReal.ofReal (C * Real.rpow (n : ℝ) (1 / 4))

Sources

• Lee and Vempala, Ann. of Math. 199 (2024), 1--104; optimizationproblems constants/20c.md, LV2024 row.

Uses 1

Statement usesDimensional KLS constant

TheoremChen's subpolynomial bound on the KLS constant, weaker form#●ready to prove

There are a real \(C > 0\) and an integer \(N \ge 3\) such that for every \(n \ge N\) the dimensional KLS constant \(\psi_n \in [0, \infty]\) satisfies \(\psi_n \le \exp\bigl(C \sqrt{\log n} \, \log \log n\bigr)\).

public theorem_wanted chen2021_bound :
    ∃ C : ℝ, 0 < C ∧ ∃ N : ℕ, 3 ≤ N ∧ ∀ n : ℕ, N ≤ n →
      dimensionalKlsConstant n ≤
        ENNReal.ofReal (Real.exp (C * Real.sqrt (Real.log n) * Real.log (Real.log n)))

Sources

• Chen, GAFA 31 (2021), 34--61; optimizationproblems constants/20c.md. Jambulapati--Lee--Vempala v1 quotes the stronger exponent sqrt(log n * log(log n)).

Uses 1

Statement usesDimensional KLS constant

TheoremKlartag–Lehec polylogarithmic bound on the KLS constant#●ready to prove

There are a real \(C > 0\) and an integer \(N \ge 3\) such that for every \(n \ge N\) the dimensional KLS constant \(\psi_n \in [0, \infty]\) satisfies \(\psi_n \le C (\log n)^5\).

public theorem_wanted klartagLehec2022_bound :
    ∃ C : ℝ, 0 < C ∧ ∃ N : ℕ, 3 ≤ N ∧ ∀ n : ℕ, N ≤ n →
      dimensionalKlsConstant n ≤ ENNReal.ofReal (C * Real.rpow (Real.log n) 5)

Sources

• Klartag and Lehec, GAFA 32 (2022), 1134--1159; optimizationproblems constants/20c.md, KL2022 row.

Uses 1

Statement usesDimensional KLS constant

TheoremJambulapati–Lee–Vempala polylogarithmic bound on the KLS constant#●ready to prove

Let \(\alpha = 1 + \bigl(1 + 7\sqrt{2} + \sqrt{53 - 4\sqrt{2}}\bigr)/8\). There are a real \(C > 0\) and an integer \(N \ge 3\) such that for every \(n \ge N\) the dimensional KLS constant \(\psi_n \in [0, \infty]\) satisfies \(\psi_n \le C (\log n)^{\alpha}\).

The exponent is kept in exact algebraic form rather than as a rounded decimal.

public theorem_wanted jambulapatiLeeVempala2022_bound :
    ∃ C : ℝ, 0 < C ∧ ∃ N : ℕ, 3 ≤ N ∧ ∀ n : ℕ, N ≤ n →
      dimensionalKlsConstant n ≤ ENNReal.ofReal
        (C * Real.rpow (Real.log n)
          (1 + (1 + 7 * Real.sqrt 2 + Real.sqrt (53 - 4 * Real.sqrt 2)) / 8))

Sources

• arXiv:2208.11644v1, Theorem 22 and the preceding KLS/thin-shell comparison.

Uses 1

Statement usesDimensional KLS constant

TheoremLehec's reported polylogarithmic bound on the KLS constant, weakened#●ready to prove

There are a real \(C > 0\) and an integer \(N \ge 3\) such that for every \(n \ge N\) the dimensional KLS constant \(\psi_n \in [0, \infty]\) satisfies \(\psi_n \le C (\log n)^{3.083}\).

The exponent \(3.083\) lies just above Lehec's reported exponent \(3.082\ldots\), which the primary gives only to this decimal precision; \(3.083\) is not claimed to be the exact exponent.

public theorem_wanted lehec_reported_bound_weaker_specialization :
    ∃ C : ℝ, 0 < C ∧ ∃ N : ℕ, 3 ≤ N ∧ ∀ n : ℕ, N ≤ n →
      dimensionalKlsConstant n ≤ ENNReal.ofReal (C * Real.rpow (Real.log n) (3083 / 1000))

Sources

• Klartag, arXiv:2303.14938v1, Introduction, personal-communication paragraph.

Uses 1

Statement usesDimensional KLS constant

TheoremKlartag's square-root-logarithmic bound on the KLS constant#●ready to prove

There is a real \(C > 0\) such that for every integer \(n \ge 2\) the dimensional KLS constant \(\psi_n \in [0, \infty]\) satisfies \(\psi_n \le C \sqrt{\log n}\).

public theorem_wanted klartag2023_bound :
    ∃ C : ℝ, 0 < C ∧ ∀ n : ℕ, 2 ≤ n →
      dimensionalKlsConstant n ≤ ENNReal.ofReal (C * Real.sqrt (Real.log n))

Sources

• Klartag, arXiv:2303.14938v1, Theorem 1.2.

Uses 1

Statement usesDimensional KLS constant

TheoremInverse Cheeger constant of the standard Gaussian#●ready to prove

For every \(n \ge 1\), the standard Gaussian measure on \(\mathbb{R}^n\) has inverse Cheeger constant exactly \(\sqrt{\pi/2}\).

public theorem_wanted stdGaussian_inverseCheeger (n : ℕ) (hn : 0 < n) :
    inverseCheegerConstant
      (ProbabilityTheory.stdGaussian (EuclideanSpace ℝ (Fin n))) =
        ENNReal.ofReal (Real.sqrt (Real.pi / 2))

Sources

• optimizationproblems constants/20c.md, classical Gaussian row; the Gaussian isoperimetric theorem supplies the minimizing half-space claim.

Uses 1

Statement usesInverse Cheeger constant

TheoremA lower bound for the KLS constant#●ready to prove

The KLS constant is at least \(\sqrt{\pi/2}\).

The bound comes from the standard Gaussian measure in any dimension \(n \ge 1\), whose inverse Cheeger constant is \(\sqrt{\pi/2}\).

public theorem_wanted sqrtPiDivTwo_le_klsConstant :
    ENNReal.ofReal (Real.sqrt (Real.pi / 2)) ≤ klsConstant

Sources

• optimizationproblems constants/20c.md, classical Gaussian lower-bound row.

Uses 1

Statement usesKLS constant

TheoremLower Poincaré–Cheeger comparison with coefficient 1/π#●ready to prove

Let \(n \ge 1\) and let \(\mu\) be an isotropic log-concave probability measure on \(\mathbb{R}^n\), with inverse Cheeger constant \(\psi(\mu) \in [0, \infty]\) and smooth Poincaré constant \(C_P(\mu) \in [0, \infty]\). Then \(\frac{1}{\pi} \psi(\mu)^2 \le C_P(\mu)\).

public theorem_wanted catalogue_poincare_lower_bound {n : ℕ} (hn : 0 < n)
    {μ : Measure (EuclideanSpace ℝ (Fin n))} (hμ : IsIsotropicLogConcave μ) :
    ENNReal.ofReal (1 / Real.pi) * inverseCheegerConstant μ ^ 2 ≤
      smoothPoincareConstant μ

Sources

• optimizationproblems constants/20c.md, Poincare comparison display. Klartag arXiv:2303.14938v1 states the weaker lower coefficient 1/9, not 1/pi.

Uses 3

Statement usesInverse Cheeger constant · Smooth Poincaré constant · Isotropic log-concave probability measures

TheoremLower Poincaré–Cheeger comparison with coefficient 1/9#●ready to prove

Let \(n \ge 1\) and let \(\mu\) be an isotropic log-concave probability measure on \(\mathbb{R}^n\), with inverse Cheeger constant \(\psi(\mu) \in [0, \infty]\) and smooth Poincaré constant \(C_P(\mu) \in [0, \infty]\). Then \(\frac{1}{9} \psi(\mu)^2 \le C_P(\mu)\).

public theorem_wanted klartag2023_poincare_lower_bound {n : ℕ} (hn : 0 < n)
    {μ : Measure (EuclideanSpace ℝ (Fin n))} (hμ : IsIsotropicLogConcave μ) :
    ENNReal.ofReal (1 / 9) * inverseCheegerConstant μ ^ 2 ≤
      smoothPoincareConstant μ

Sources

• Klartag, arXiv:2303.14938v1, equation comparing psi and C_P. The locally Lipschitz-to-smooth approximation remains part of the requested proof.

Uses 3

Statement usesInverse Cheeger constant · Smooth Poincaré constant · Isotropic log-concave probability measures

TheoremCheeger's inequality for isotropic log-concave measures#●ready to prove

Let \(n \ge 1\), let \(\mu\) be an isotropic log-concave probability measure on \(\mathbb{R}^n\), and let \(\psi_\mu \in [0, \infty]\) be the inverse Cheeger constant of \(\mu\). Then the smooth Poincaré constant of \(\mu\) is at most \(4 \psi_\mu^2\).

public theorem_wanted poincare_cheeger_upper_bound {n : ℕ} (hn : 0 < n)
    {μ : Measure (EuclideanSpace ℝ (Fin n))} (hμ : IsIsotropicLogConcave μ) :
    smoothPoincareConstant μ ≤ 4 * inverseCheegerConstant μ ^ 2

Sources

• optimizationproblems constants/20c.md, comparison display, and Klartag, arXiv:2303.14938v1, Introduction.

Uses 3

Statement usesInverse Cheeger constant · Smooth Poincaré constant · Isotropic log-concave probability measures

TheoremDimensional KLS constant versus thin-shell variance, up to a squared logarithm#●ready to prove

Let \(\Sigma \in [0, \infty]\) be the thin-shell variance constant: the supremum, over all dimensions \(m \ge 1\) and all isotropic log-concave probability measures \(\mu\) on \(\mathbb{R}^m\), of \(\frac{1}{m} \int (\lVert x \rVert^2 - m)^2 \, d\mu(x)\). There is a real \(C > 0\) such that for every integer \(n \ge 3\) the dimensional KLS constant \(\psi_n \in [0, \infty]\) satisfies \(\psi_n^2 \le C (\log n)^2 \, \Sigma\).

public theorem_wanted kls_le_thinShell_variance_log_squared :
    ∃ C : ℝ, 0 < C ∧ ∀ n : ℕ, 3 ≤ n →
      dimensionalKlsConstant n ^ 2 ≤
        ENNReal.ofReal (C * Real.log n ^ 2) * thinShellVarianceConstant

Sources

• Jambulapati--Lee--Vempala, arXiv:2208.11644v1, KLS/thin-shell comparison.

Uses 2

Statement usesDimensional KLS constant · Thin-shell variance constant

22 fully proved13 ready to prove

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.