Thin-shell conjecture

DefinitionLog-concave densities#✓fully proved

A function \(f : \mathbb{R}^n \to \mathbb{R}\) is a log-concave density when it is measurable, \(f(x) \ge 0\) for every \(x\), and \(f(x)^{1-t} f(y)^t \le f((1-t)x + ty)\) for all \(x, y \in \mathbb{R}^n\) and every real \(t\) with \(0 < t < 1\).

No integrability or normalization of \(f\) is required.

def IsLogConcaveDensity {n : ℕ} (f : EuclideanSpace ℝ (Fin n) → ℝ) : Prop :=
  Measurable f ∧ (∀ x, 0 ≤ f x) ∧
    ∀ x y : EuclideanSpace ℝ (Fin n), ∀ t : ℝ, 0 < t → t < 1 →
      Real.rpow (f x) (1 - t) * Real.rpow (f y) t ≤ f ((1 - t) • x + t • y)

Used by 7

Used byUniform law of a convex body · Isotropic log-concave laws have identity covariance · Constant densities on convex sets are log-concave · Log-concave law · The uniform law on (−1, 1) is not isotropic log-concave · The uniform law on (−√3, √3) is isotropic log-concave · Isotropic log-concave probability measures

DefinitionIsotropic log-concave probability measures#✓fully proved

A measure \(\mu\) on \(\mathbb{R}^n\) is isotropic log-concave when it is a probability measure, it has density \(f\) with respect to Lebesgue measure for some log-concave density \(f\), and for all coordinates \(i, j\) the functions \(x \mapsto x_i\) and \(x \mapsto x_i x_j\) are \(\mu\)-integrable with \(\int x_i \, d\mu(x) = 0\) and \(\int x_i x_j \, d\mu(x) = \delta_{ij}\), that is, \(1\) if \(i = j\) and \(0\) otherwise.

def IsIsotropicLogConcave {n : ℕ} (μ : Measure (EuclideanSpace ℝ (Fin n))) : Prop :=
  IsProbabilityMeasure μ ∧
    (∃ f : EuclideanSpace ℝ (Fin n) → ℝ, IsLogConcaveDensity f ∧
      μ = volume.withDensity (fun x => ENNReal.ofReal (f x))) ∧
    (∀ i : Fin n, Integrable (fun x => x i) μ ∧ (∫ x, x i ∂μ) = 0) ∧
    ∀ i j : Fin n, Integrable (fun x => x i * x j) μ ∧
      (∫ x, x i * x j ∂μ) = if i = j then 1 else 0

Uses 1 · Used by 22

Statement usesLog-concave densities

Used byIsotropic log-concave laws have identity covariance · Squared-radius thin-shell width · The uniform law on (−1, 1) is not isotropic log-concave · The uniform law on (−√3, √3) is isotropic log-concave · Lower 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 · 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 · Klartag–Lehec thin-shell variance bound · The thin-shell variance constant bounds the normalized radius variance of isotropic log-concave measures · The thin-shell variance constant bounds the radius fluctuation · The standard Gaussian has normalized radius variance 2 · Thin-shell variance constant · Characterization of bounds on the thin-shell variance constant · A uniform variance bound makes the thin-shell variance constant finite · Thin-shell width · Thin-shell width is at most the square root of the variance constant · The isotropic cube has normalized radius variance 4/5

DefinitionNormalized radius variance#✓fully proved

For a measure \(\mu\) on \(\mathbb{R}^n\), the normalized radius variance of \(\mu\) is \(\frac{1}{n} \int (\|x\|^2 - n)^2 \, d\mu(x)\), computed in \([0, \infty]\), where \(\|x\|\) is the Euclidean norm (for \(n = 0\) the integral is \(0\) and so is the value).

When \(\mu\) is a probability measure with \(\int \|x\|^2 \, d\mu(x) = n\), as for an isotropic one, this is the variance of \(\|x\|^2\) divided by \(n\).

noncomputable def normalizedRadiusVariance {n : ℕ}
    (μ : Measure (EuclideanSpace ℝ (Fin n))) : ℝ≥0∞ :=
  (∫⁻ x, ENNReal.ofReal ((‖x‖ ^ 2 - (n : ℝ)) ^ 2) ∂μ) / (n : ℝ≥0∞)

Used by 11

Used bySquared-radius thin-shell width · Thin-shell variance bound for the uniform law on (−√3, √3) · Klartag–Lehec thin-shell variance bound · The thin-shell variance constant bounds the normalized radius variance of isotropic log-concave measures · The thin-shell variance constant bounds the radius fluctuation · Radius fluctuation is bounded by the normalized radius variance · The standard Gaussian has normalized radius variance 2 · Thin-shell variance constant · Characterization of bounds on the thin-shell variance constant · A uniform variance bound makes the thin-shell variance constant finite · The isotropic cube has normalized radius variance 4/5

DefinitionThin-shell variance constant#✓fully proved

Write \(|x|\) for the Euclidean norm. The thin-shell variance constant is the supremum, taken in \([0, \infty]\), of the normalized radius variance \(\frac{1}{n} \int (|x|^2 - n)^2 \, d\mu(x)\) over all dimensions \(n \ge 1\) and all isotropic log-concave probability measures \(\mu\) on \(\mathbb{R}^n\).

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

Uses 2 · Used by 12

Statement usesIsotropic log-concave probability measures · Normalized radius variance

Used byRadius fluctuation of the uniform law on (−√3, √3) · Thin-shell variance bound for the uniform law on (−√3, √3) · Dimensional KLS constant versus thin-shell variance, up to a squared logarithm · Cube lower bound for the thin-shell variance constant · The thin-shell variance constant bounds the normalized radius variance of isotropic log-concave measures · The thin-shell variance constant bounds the radius fluctuation · Characterization of bounds on the thin-shell variance constant · The thin-shell variance constant is finite · A uniform variance bound makes the thin-shell variance constant finite · The thin-shell variance constant is nonnegative · Thin-shell width is at most the square root of the variance constant · The thin-shell variance constant is at least 2

DefinitionThin-shell width#✓fully proved

Write \(|x|\) for the Euclidean norm. For \(n \in \mathbb{N}\), the thin-shell width in dimension \(n\) is the square root of the supremum, taken in \([0, \infty]\), of \(\int (|x| - \sqrt{n})^2 \, d\mu(x)\) over all isotropic log-concave probability measures \(\mu\) on \(\mathbb{R}^n\), with \(\sqrt{\infty} = \infty\).

noncomputable def thinShellWidth (n : ℕ) : ℝ≥0∞ :=
  ENNReal.rpow (sSup {v | ∃ μ : Measure (EuclideanSpace ℝ (Fin n)),
    IsIsotropicLogConcave μ ∧
      (∫⁻ x, ENNReal.ofReal ((‖x‖ - Real.sqrt (n : ℝ)) ^ 2) ∂μ) = v}) (1 / 2)

Uses 1 · Used by 12

Statement usesIsotropic log-concave probability measures

Used byChen's thin-shell bound · Fleury's thin-shell bound · Guan's thin-shell bound · Guédon–Milman thin-shell bound · Jambulapati–Lee–Vempala thin-shell bound · Klartag–Lehec polylogarithmic thin-shell bound · Klartag–Lehec bounded thin-shell width · Klartag's first thin-shell bound · Klartag's power-law thin-shell bound · Klartag's square-root-logarithmic thin-shell bound · Lee–Vempala thin-shell bound · Thin-shell width is at most the square root of the variance constant

TheoremElementary radius deviation bound#✓fully proved

For all real numbers \(r \ge 0\) and \(d > 0\), \((r - \sqrt{d})^2 \le (r^2 - d)^2 / d\).

theorem radius_deviation_sq_le {r d : ℝ} (hr : 0 ≤ r) (hd : 0 < d) :
    (r - Real.sqrt d) ^ 2 ≤ (r ^ 2 - d) ^ 2 / d

Used by 1

Used byRadius fluctuation is bounded by the normalized radius variance

TheoremRadius fluctuation is bounded by the normalized radius variance#✓fully proved

For every \(n > 0\) and every measure \(\mu\) on \(\mathbb{R}^n\), the integral \(\int (\|x\| - \sqrt{n})^2 \, d\mu(x)\), taken in \([0, \infty]\) with \(\|x\|\) the Euclidean norm, is at most the normalized radius variance of \(\mu\).

The bound holds even when the moments are infinite.

theorem radius_fluctuation_le_normalized_variance {n : ℕ} (hn : 0 < n)
    (μ : Measure (EuclideanSpace ℝ (Fin n))) :
    (∫⁻ x, ENNReal.ofReal ((‖x‖ - Real.sqrt (n : ℝ)) ^ 2) ∂μ) ≤
      normalizedRadiusVariance μ

Uses 2 · Used by 1

Statement usesNormalized radius variance

Proof usesElementary radius deviation bound

Used byThe thin-shell variance constant bounds the radius fluctuation

TheoremThe thin-shell variance constant bounds the normalized radius variance of isotropic log-concave measures#✓fully proved

The thin-shell variance constant bounds the normalized radius variance of isotropic log-concave measures. For every \(n > 0\) and every isotropic log-concave probability measure \(\mu\) on \(\mathbb{R}^n\), the normalized radius variance of \(\mu\) is at most the thin-shell variance constant.

theorem normalizedRadiusVariance_le_constant {n : ℕ} (hn : 0 < n)
    {μ : Measure (EuclideanSpace ℝ (Fin n))} (hμ : IsIsotropicLogConcave μ) :
    normalizedRadiusVariance μ ≤ thinShellVarianceConstant

Uses 3 · Used by 3

Statement usesIsotropic log-concave probability measures · Normalized radius variance · Thin-shell variance constant

Used byThin-shell variance bound for the uniform law on (−√3, √3) · The thin-shell variance constant bounds the radius fluctuation · Characterization of bounds on the thin-shell variance constant

TheoremCharacterization of bounds on the thin-shell variance constant#✓fully proved

For every \(C \in [0, \infty]\), the thin-shell variance constant is at most \(C\) if and only if, for every \(n > 0\) and every isotropic log-concave probability measure \(\mu\) on \(\mathbb{R}^n\), the normalized radius variance of \(\mu\) is at most \(C\).

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

Uses 4 · Used by 1

Statement usesIsotropic log-concave probability measures · Normalized radius variance · Thin-shell variance constant

Proof usesThe thin-shell variance constant bounds the normalized radius variance of isotropic log-concave measures

Used byA uniform variance bound makes the thin-shell variance constant finite

TheoremThe thin-shell variance constant bounds the radius fluctuation#✓fully proved

For every \(n > 0\) and every isotropic log-concave probability measure \(\mu\) on \(\mathbb{R}^n\), the integral \(\int (\|x\| - \sqrt{n})^2 \, d\mu(x)\), taken in \([0, \infty]\) with \(\|x\|\) the Euclidean norm, is at most the thin-shell variance constant.

theorem radius_fluctuation_le_constant {n : ℕ} (hn : 0 < n)
    {μ : Measure (EuclideanSpace ℝ (Fin n))} (hμ : IsIsotropicLogConcave μ) :
    (∫⁻ x, ENNReal.ofReal ((‖x‖ - Real.sqrt (n : ℝ)) ^ 2) ∂μ) ≤
      thinShellVarianceConstant

Uses 5 · Used by 2

Statement usesIsotropic log-concave probability measures · Thin-shell variance constant

Proof usesNormalized radius variance · The thin-shell variance constant bounds the normalized radius variance of isotropic log-concave measures · Radius fluctuation is bounded by the normalized radius variance

Used byRadius fluctuation of the uniform law on (−√3, √3) · Thin-shell width is at most the square root of the variance constant

TheoremThe thin-shell variance constant is nonnegative#✓fully proved

The thin-shell variance constant, a value in \([0, \infty]\), is at least \(0\).

theorem thinShellVarianceConstant_nonneg : 0 ≤ thinShellVarianceConstant

Uses 1

Statement usesThin-shell variance constant

TheoremThin-shell width is at most the square root of the variance constant#✓fully proved

For every dimension \(n \ge 1\), the thin-shell width in dimension \(n\) is at most the square root of the thin-shell variance constant, computed in \([0, \infty]\) with \(\sqrt{\infty} = \infty\).

theorem thinShellWidth_le_sqrt_constant {n : ℕ} (hn : 0 < n) :
    thinShellWidth n ≤ ENNReal.rpow thinShellVarianceConstant (1 / 2)

Uses 4

Statement usesThin-shell variance constant · Thin-shell width

Proof usesIsotropic log-concave probability measures · The thin-shell variance constant bounds the radius fluctuation

TheoremA uniform variance bound makes the thin-shell variance constant finite#✓fully proved

If \(C\) is a real number such that for every \(n > 0\) and every isotropic log-concave probability measure \(\mu\) on \(\mathbb{R}^n\) the normalized radius variance of \(\mu\) is at most \(\max(C, 0)\), then the thin-shell variance constant is finite.

theorem thinShellVarianceConstant_lt_top_of_bound {C : ℝ}
    (hC : ∀ n : ℕ, 0 < n → ∀ μ : Measure (EuclideanSpace ℝ (Fin n)),
      IsIsotropicLogConcave μ → normalizedRadiusVariance μ ≤ ENNReal.ofReal C) :
    thinShellVarianceConstant < ⊤

Uses 4

Statement usesIsotropic log-concave probability measures · Normalized radius variance · Thin-shell variance constant

Proof usesCharacterization of bounds on the thin-shell variance constant

TheoremKlartag's first thin-shell bound#●ready to prove

There are a real \(C > 0\) and a natural number \(N \ge 3\) such that for every natural number \(n \ge N\) the thin-shell width \(\sigma_n \in [0, \infty]\) of dimension \(n\) satisfies \(\sigma_n \le C \sqrt{n / \log n}\).

This is Klartag's first bound in the weaker form tabulated by the optimization catalogue.

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

Sources

• Klartag, Invent. Math. 168 (2007), 91--131; catalogue constants/20a.md.

Uses 1

Statement usesThin-shell width

TheoremKlartag's power-law thin-shell bound#●ready to prove

For every \(\varepsilon > 0\) there are a constant \(C > 0\) and an integer \(N \ge 3\) such that for every dimension \(n \ge N\) the thin-shell width \(\sigma_n \in [0, \infty]\) satisfies \(\sigma_n \le C n^{2/5 + \varepsilon}\). Here \(\sigma_n\) is the square root of the supremum of \(\mathbb{E}\,(|X| - \sqrt{n})^2\) over isotropic log-concave random vectors \(X\) in \(\mathbb{R}^n\).

public theorem_wanted klartag2007b_width_bound :
    ∀ ε : ℝ, 0 < ε → ∃ C : ℝ, 0 < C ∧ ∃ N : ℕ, 3 ≤ N ∧ ∀ n : ℕ, N ≤ n →
      thinShellWidth n ≤ ENNReal.ofReal (C * Real.rpow (n : ℝ) (2 / 5 + ε))

Sources

• Klartag, J. Funct. Anal. 245 (2007), 284--310; catalogue constants/20a.md.

Uses 1

Statement usesThin-shell width

TheoremFleury's thin-shell bound#●ready to prove

There are a real \(C > 0\) and a natural number \(N \ge 3\) such that for every natural number \(n \ge N\) the thin-shell width \(\sigma_n \in [0, \infty]\) of dimension \(n\) satisfies \(\sigma_n \le C n^{3/8}\).

public theorem_wanted fleury2010_width_bound :
    ∃ C : ℝ, 0 < C ∧ ∃ N : ℕ, 3 ≤ N ∧ ∀ n : ℕ, N ≤ n →
      thinShellWidth n ≤ ENNReal.ofReal (C * Real.rpow (n : ℝ) (3 / 8))

Sources

• Fleury, J. Funct. Anal. 259 (2010), 832--841; catalogue constants/20a.md.

Uses 1

Statement usesThin-shell width

TheoremGuédon–Milman thin-shell bound#●ready to prove

There are a real \(C > 0\) and a natural number \(N \ge 3\) such that for every natural number \(n \ge N\) the thin-shell width \(\sigma_n \in [0, \infty]\) of dimension \(n\) satisfies \(\sigma_n \le C n^{1/3}\).

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

Sources

• Guedon and Milman, GAFA 21 (2011), 1043--1068; catalogue constants/20a.md.

Uses 1

Statement usesThin-shell width

TheoremLee–Vempala thin-shell bound#●ready to prove

There are a constant \(C > 0\) and an integer \(N \ge 3\) such that for every dimension \(n \ge N\) the thin-shell width \(\sigma_n \in [0, \infty]\) satisfies \(\sigma_n \le C n^{1/4}\). Here \(\sigma_n\) is the square root of the supremum of \(\mathbb{E}\,(|X| - \sqrt{n})^2\) over isotropic log-concave random vectors \(X\) in \(\mathbb{R}^n\).

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

Sources

• Lee and Vempala, FOCS 2017, 998--1007; catalogue constants/20a.md.

Uses 1

Statement usesThin-shell width

TheoremChen's thin-shell bound#●ready to prove

For every real \(\varepsilon > 0\) there is a natural number \(N \ge 3\) such that for every natural number \(n \ge N\) the thin-shell width \(\sigma_n \in [0, \infty]\) of dimension \(n\) satisfies \(\sigma_n \le \exp\big((\log n)^{1/2 + \varepsilon}\big)\).

There is no constant multiplier inside the exponential.

public theorem_wanted chen2021_width_bound :
    ∀ ε : ℝ, 0 < ε → ∃ N : ℕ, 3 ≤ N ∧ ∀ n : ℕ, N ≤ n →
      thinShellWidth n ≤
        ENNReal.ofReal (Real.exp (Real.rpow (Real.log n) (1 / 2 + ε)))

Sources

• Chen, GAFA 31 (2021), 34--61; catalogue constants/20a.md.

Uses 1

Statement usesThin-shell width

TheoremKlartag–Lehec polylogarithmic thin-shell bound#●ready to prove

There are a real \(C > 0\) and a natural number \(N \ge 3\) such that for every natural number \(n \ge N\) the thin-shell width \(\sigma_n \in [0, \infty]\) of dimension \(n\) satisfies \(\sigma_n \le C (\log n)^4\).

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

Sources

• Klartag and Lehec, GAFA 32 (2022), 1134--1159; catalogue constants/20a.md.

Uses 1

Statement usesThin-shell width

TheoremJambulapati–Lee–Vempala thin-shell bound#●ready to prove

Let \(\alpha = \big(1 + 7\sqrt{2} + \sqrt{53 - 4\sqrt{2}}\big)/8\). There are a real \(C > 0\) and a natural number \(N \ge 3\) such that for every natural number \(n \ge N\) the thin-shell width \(\sigma_n \in [0, \infty]\) of dimension \(n\) satisfies \(\sigma_n \le C (\log n)^{\alpha}\).

The exponent \(\alpha\) is algebraic, not rational; the paper bounds it by \(2.2226\). The paper proves this bound for the square root of the normalized variance of the squared radius, which bounds the thin-shell width from above.

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

Sources

• Jambulapati, Lee and Vempala, arXiv:2208.11644v1, Theorem 22.

Uses 1

Statement usesThin-shell width

TheoremKlartag's square-root-logarithmic thin-shell bound#●ready to prove

There are a constant \(C > 0\) and an integer \(N \ge 3\) such that for every dimension \(n \ge N\) the thin-shell width \(\sigma_n \in [0, \infty]\) satisfies \(\sigma_n \le C \sqrt{\log n}\). Here \(\sigma_n\) is the square root of the supremum of \(\mathbb{E}\,(|X| - \sqrt{n})^2\) over isotropic log-concave random vectors \(X\) in \(\mathbb{R}^n\), and \(\log\) is the natural logarithm.

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

Sources

• Klartag, Ars Inveniendi Analytica (2023), Paper 4; catalogue constants/20a.md.

Uses 1

Statement usesThin-shell width

TheoremGuan's thin-shell bound#●ready to prove

There are a real \(C > 0\) and a natural number \(N \ge 3\) such that for every natural number \(n \ge N\) the thin-shell width \(\sigma_n \in [0, \infty]\) of dimension \(n\) satisfies \(\sigma_n \le C \log \log n\).

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

Sources

• Guan, arXiv:2412.09075; catalogue constants/20a.md.

Uses 1

Statement usesThin-shell width

TheoremKlartag–Lehec thin-shell variance bound#●ready to prove

There is a real \(C > 0\) such that for every natural number \(n \ge 1\) and every isotropic log-concave measure \(\mu\) on \(\mathbb{R}^n\), the normalized radius variance \(\frac{1}{n} \int (|x|^2 - n)^2 \, d\mu(x)\) is at most \(C\).

public theorem_wanted klartagLehec2025_variance_bound :
    ∃ C : ℝ, 0 < C ∧ ∀ n : ℕ, 0 < n →
      ∀ μ : Measure (EuclideanSpace ℝ (Fin n)), IsIsotropicLogConcave μ →
        normalizedRadiusVariance μ ≤ ENNReal.ofReal C

Sources

• arXiv:2507.15495v1, Theorem 1.1. The constant is not optimized or made explicit.

Uses 2

Statement usesIsotropic log-concave probability measures · Normalized radius variance

TheoremKlartag–Lehec bounded thin-shell width#●ready to prove

There is a real \(C > 0\) such that for every natural number \(n \ge 1\) the thin-shell width \(\sigma_n \in [0, \infty]\) of dimension \(n\) satisfies \(\sigma_n \le C\).

public theorem_wanted klartagLehec2025_width_bound :
    ∃ C : ℝ, 0 < C ∧ ∀ n : ℕ, 0 < n → thinShellWidth n ≤ ENNReal.ofReal C

Sources

• Klartag and Lehec, arXiv:2507.15495v1, Introduction and Theorem 1.1.

Uses 1

Statement usesThin-shell width

TheoremThe thin-shell variance constant is finite#●ready to prove

The thin-shell variance constant, the supremum in \([0, \infty]\) of the normalized radius variances \(\frac{1}{n} \int (|x|^2 - n)^2 \, d\mu(x)\) over all dimensions \(n \ge 1\) and all isotropic log-concave probability measures \(\mu\) on \(\mathbb{R}^n\), is finite.

public theorem_wanted thinShellVarianceConstant_lt_top :
    thinShellVarianceConstant < ⊤

Sources

• Klartag and Lehec, arXiv:2507.15495v1, Theorem 1.1.

Uses 1

Statement usesThin-shell variance constant

TheoremThe standard Gaussian has normalized radius variance 2#●ready to prove

For every dimension \(n \ge 1\), the standard Gaussian measure \(\gamma_n\) on \(\mathbb{R}^n\) is isotropic log-concave (a probability measure with a log-concave Lebesgue density, mean \(0\) and identity covariance), and its normalized radius variance \(\frac{1}{n} \int (|x|^2 - n)^2 \, d\gamma_n(x)\) equals \(2\).

public theorem_wanted stdGaussian_isotropic_variance (n : ℕ) (hn : 0 < n) :
    IsIsotropicLogConcave (ProbabilityTheory.stdGaussian (EuclideanSpace ℝ (Fin n))) ∧
      normalizedRadiusVariance
        (ProbabilityTheory.stdGaussian (EuclideanSpace ℝ (Fin n))) = 2

Sources

• Klartag--Lehec, arXiv:2507.15495v1, Introduction.

Uses 2

Statement usesIsotropic log-concave probability measures · Normalized radius variance

TheoremThe isotropic cube has normalized radius variance 4/5#●ready to prove

For every dimension \(n \ge 1\), let \(\mu\) be the uniform probability measure on the cube \([-\sqrt{3}, \sqrt{3}]^n \subset \mathbb{R}^n\) (Lebesgue measure restricted to the cube and divided by its volume). Then \(\mu\) is isotropic log-concave (a probability measure with a log-concave Lebesgue density, mean \(0\) and identity covariance), and its normalized radius variance \(\frac{1}{n} \int (|x|^2 - n)^2 \, d\mu(x)\) equals \(4/5\).

The cube is scaled to covariance identity, so this is the unit-variance convention.

public theorem_wanted uniformCube_isotropic_variance (n : ℕ) (hn : 0 < n) :
    let μ := ProbabilityTheory.cond
      (volume : Measure (EuclideanSpace ℝ (Fin n)))
      {x | ∀ i : Fin n, |x i| ≤ Real.sqrt 3}
    IsIsotropicLogConcave μ ∧ normalizedRadiusVariance μ = ENNReal.ofReal (4 / 5)

Sources

• Klartag--Lehec, arXiv:2507.15495v1, Introduction.

Uses 2

Statement usesIsotropic log-concave probability measures · Normalized radius variance

TheoremCube lower bound for the thin-shell variance constant#●ready to prove

The thin-shell variance constant, an element of \([0, \infty]\), is at least \(4/5\).

The value \(4/5\) is the exact normalized radius variance of the uniform law on a cube scaled to identity covariance.

public theorem_wanted fourFifths_le_thinShellVarianceConstant :
    ENNReal.ofReal (4 / 5) ≤ thinShellVarianceConstant

Sources

• Klartag and Lehec, arXiv:2507.15495v1, Introduction.

Uses 1

Statement usesThin-shell variance constant

TheoremThe thin-shell variance constant is at least 2#●ready to prove

The thin-shell variance constant, the supremum in \([0, \infty]\) of the normalized radius variances \(\frac{1}{n} \int (|x|^2 - n)^2 \, d\mu(x)\) over all dimensions \(n \ge 1\) and all isotropic log-concave probability measures \(\mu\) on \(\mathbb{R}^n\), is at least \(2\).

The lower bound comes from the standard Gaussian, whose normalized radius variance is \(2\) in every dimension.

public theorem_wanted two_le_thinShellVarianceConstant :
    2 ≤ thinShellVarianceConstant

Sources

• Klartag and Lehec, arXiv:2507.15495v1, Introduction.

Uses 1

Statement usesThin-shell variance constant

13 fully proved17 ready to prove

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.