Isotropic constant of log-concave laws

DefinitionCovariance matrix#✓fully proved

For a measure \(\mu\) on \(\mathbb{R}^n\), the covariance matrix of \(\mu\) is the \(n \times n\) real matrix whose \((i, j)\) entry is \(\int (x_i - m_i)(x_j - m_j) \, d\mu(x)\), where \(m_i = \int x_i \, d\mu(x)\) is the mean of the \(i\)-th coordinate.

noncomputable def covarianceMatrix {n : ℕ}
    (μ : Measure (EuclideanSpace ℝ (Fin n))) : Matrix (Fin n) (Fin n) ℝ :=
  fun i j => ProbabilityTheory.covariance (fun x => x i) (fun x => x j) μ

Sources

• constants/20b.md, covariance definition.

Used by 6

Used byIsotropic constant of a convex body · The entropy and volume isotropic constants of a convex body agree · Isotropic log-concave laws have identity covariance · Covariance matrices of log-concave laws are positive semidefinite · Cube lower bound for the supremal isotropic constant · Isotropic constant of a log-concave law

DefinitionDifferential entropy#✓fully proved

For a function \(f \colon \mathbb{R}^n \to \mathbb{R}\), usually the Lebesgue density of a probability law, the differential entropy of \(f\) is \(-\int_{\mathbb{R}^n} f(x) \log f(x) \, dx\), with the natural logarithm and \(0 \log 0 = 0\).

noncomputable def differentialEntropy {n : ℕ} (f : EuclideanSpace ℝ (Fin n) → ℝ) : ℝ :=
  -(∫ x, f x * Real.log (f x))

Sources

• constants/20b.md, Ent(μ)=-∫f log f.

Used by 3

Used byEntropy of the uniform density of a convex body · The entropy and volume isotropic constants of a convex body agree · Isotropic constant of a log-concave law

StructureFull-dimensional convex body#✓fully proved

For a natural number \(n\), a full-dimensional convex body in dimension \(n\) is a nonempty compact convex set \(K\) in the Euclidean space \(\mathbb{R}^n\) whose interior is nonempty, where \(n\) is required to be positive.

structure FullDimensionalBody (n : ℕ) where
  body : ConvexBody (EuclideanSpace ℝ (Fin n))
  dimension_pos : 0 < n
  interior_nonempty : (interior (body : Set (EuclideanSpace ℝ (Fin n)))).Nonempty

Sources

• constants/20b.md, convex-body domain.

Used by 16

Used byUniform density of a convex body · Entropy of the uniform density of a convex body · The uniform law on a convex body as an intrinsic log-concave law · Isotropic constant of a convex body · Uniform distribution on a convex body · The uniform law on a convex body spans the whole space · Uniform law of a convex body · The entropy and volume isotropic constants of a convex body agree · Supremum of isotropic constants of symmetric convex bodies · Supremum of isotropic constants in a fixed dimension · Body isotropic constants are bounded by the law supremum · Symmetric interval as a convex body · Cube lower bound for the supremal isotropic constant · Centrally symmetric convex body · Unit interval body · Membership in the unit interval body

StructureLog-concave law#✓fully proved

For a positive integer \(n\), a log-concave law on \(\mathbb{R}^n\) is a probability measure \(\mu\) on \(\mathbb{R}^n\) together with a Lebesgue density \(f\) of \(\mu\) that is log-concave: \(f\) is measurable and nonnegative, and \(f((1-t)x + ty) \ge f(x)^{1-t} f(y)^t\) for all \(x, y \in \mathbb{R}^n\) and \(0 < t < 1\). Moreover every coordinate \(x_i\) and every product \(x_i x_j\) is \(\mu\)-integrable, and \(f \log f\) is Lebesgue integrable.

structure LogConcaveLaw (n : ℕ) where
  dimension_pos : 0 < n
  law : Measure (EuclideanSpace ℝ (Fin n))
  probability : IsProbabilityMeasure law
  density : EuclideanSpace ℝ (Fin n) → ℝ
  logConcave : ThinShell.IsLogConcaveDensity density
  law_eq : law = volume.withDensity (fun x => ENNReal.ofReal (density x))
  moment_one : ∀ i : Fin n, Integrable (fun x => x i) law
  moment_two : ∀ i j : Fin n, Integrable (fun x => x i * x j) law
  entropy_integrable : Integrable (fun x => density x * Real.log (density x)) volume

Sources

• constants/20b.md; finite moments and entropy integrability ensure the displayed real integrals do not use the non-integrable default value.

Uses 1 · Used by 10

Statement usesLog-concave densities

Used byThe uniform law on a convex body as an intrinsic log-concave law · Uniform law of a convex body · The entropy and volume isotropic constants of a convex body agree · Covariance matrices of log-concave laws are positive semidefinite · Body isotropic constants are bounded by the law supremum · Supremum of entropic isotropic constants in a fixed dimension · The entropy isotropic constant is at most the full-dimensional supremum · Isotropic constant of an intrinsic log-concave law · Log-concave law in intrinsic coordinates · Isotropic constant of a log-concave law

TheoremCovariance matrices of log-concave laws are positive semidefinite#✓fully proved

For every log-concave law \(\mu\) on \(\mathbb{R}^n\), the covariance matrix of \(\mu\) is positive semidefinite.

The proof writes the quadratic form of the covariance matrix as the integral of the square of a centered linear form.

theorem covarianceMatrix_posSemidef {n : ℕ} (μ : LogConcaveLaw n) :
    (covarianceMatrix μ.law).PosSemidef

Uses 2 · Used by 1

Statement usesLog-concave law · Covariance matrix

Used byThe entropy and volume isotropic constants of a convex body agree

TheoremIsotropic log-concave laws have identity covariance#✓fully proved

If \(\mu\) is an isotropic log-concave probability measure on \(\mathbb{R}^n\), then the covariance matrix of \(\mu\) is the \(n \times n\) identity matrix.

theorem covarianceMatrix_eq_one_of_isIsotropic {n : ℕ}
    {μ : Measure (EuclideanSpace ℝ (Fin n))} (hμ : ThinShell.IsIsotropicLogConcave μ) :
    covarianceMatrix μ = 1

Uses 3

Statement usesCovariance matrix · Isotropic log-concave probability measures

Proof usesLog-concave densities

DefinitionUniform distribution on a convex body#✓fully proved

For a full-dimensional convex body \(K\) in \(\mathbb{R}^n\), the uniform law on \(K\) is the probability measure obtained by restricting Lebesgue measure to \(K\) and dividing by the volume of \(K\); it gives a set \(A\) the mass \(\operatorname{vol}(A \cap K) / \operatorname{vol}(K)\).

noncomputable def bodyLaw {n : ℕ} (K : FullDimensionalBody n) :
    Measure (EuclideanSpace ℝ (Fin n)) :=
  ProbabilityTheory.cond volume (K.body : Set (EuclideanSpace ℝ (Fin n)))

Uses 1 · Used by 6

Statement usesFull-dimensional convex body

Used byThe uniform law on a convex body as an intrinsic log-concave law · Isotropic constant of a convex body · The uniform law on a convex body spans the whole space · Uniform law of a convex body · The entropy and volume isotropic constants of a convex body agree · Cube lower bound for the supremal isotropic constant

DefinitionIsotropic constant of a convex body#✓fully proved

For a full-dimensional convex body \(K\) in \(\mathbb{R}^n\), let \(\operatorname{Cov}(K)\) be the covariance matrix of the uniform probability law on \(K\) and let \(\operatorname{vol}(K)\) be the Lebesgue volume of \(K\). The isotropic constant of \(K\) is the real number \(L_K = \left(\det \operatorname{Cov}(K) / \operatorname{vol}(K)^2\right)^{1/(2n)}\).

noncomputable def bodyIsotropicConstant {n : ℕ} (K : FullDimensionalBody n) : ℝ :=
  Real.rpow ((covarianceMatrix (bodyLaw K)).det /
    (volume (K.body : Set (EuclideanSpace ℝ (Fin n)))).toReal ^ 2)
    (1 / (2 * (n : ℝ)))

Uses 3 · Used by 5

Statement usesFull-dimensional convex body · Uniform distribution on a convex body · Covariance matrix

Used byThe entropy and volume isotropic constants of a convex body agree · Supremum of isotropic constants of symmetric convex bodies · Supremum of isotropic constants in a fixed dimension · Body isotropic constants are bounded by the law supremum · Cube lower bound for the supremal isotropic constant

DefinitionIsotropic constant of a log-concave law#✓fully proved

For a log-concave law \(\mu\) on \(\mathbb{R}^n\) with Lebesgue density \(f\), the isotropic constant of \(\mu\) is \(L_\mu = e^{-h(f)/n} (\det \mathrm{Cov}(\mu))^{1/(2n)}\), where \(h(f) = -\int_{\mathbb{R}^n} f \log f\) is the differential entropy of \(f\) and \(\mathrm{Cov}(\mu)\) is the covariance matrix of the coordinates under \(\mu\).

noncomputable def lawIsotropicConstant {n : ℕ} (μ : LogConcaveLaw n) : ℝ :=
  Real.exp (-differentialEntropy μ.density / (n : ℝ)) *
    Real.rpow (covarianceMatrix μ.law).det (1 / (2 * (n : ℝ)))

Uses 3 · Used by 5

Statement usesLog-concave law · Covariance matrix · Differential entropy

Used byThe entropy and volume isotropic constants of a convex body agree · Body isotropic constants are bounded by the law supremum · Supremum of entropic isotropic constants in a fixed dimension · The entropy isotropic constant is at most the full-dimensional supremum · Isotropic constant of an intrinsic log-concave law

DefinitionSupremum of isotropic constants in a fixed dimension#✓fully proved

For \(n \in \mathbb{N}\), this is \(\sup_K L_K \in [0, \infty]\), the supremum of the isotropic constants \(L_K\) over all full-dimensional convex bodies \(K\) in \(\mathbb{R}^n\). Full-dimensional convex bodies are taken only in dimension \(n \ge 1\), so for \(n = 0\) the supremum is over the empty family and is \(0\).

noncomputable def dimensionBodySupremum (n : ℕ) : ℝ≥0∞ :=
  ⨆ K : FullDimensionalBody n, ENNReal.ofReal (bodyIsotropicConstant K)

Uses 2 · Used by 3

Statement usesFull-dimensional convex body · Isotropic constant of a convex body

Used bySupremum of isotropic constants of convex bodies · Body isotropic constants are bounded by the law supremum · Cube lower bound for the supremal isotropic constant

DefinitionSupremum of entropic isotropic constants in a fixed dimension#✓fully proved

For \(n \in \mathbb{N}\), this is \(\sup_\mu L_\mu \in [0, \infty]\), the supremum of the isotropic constants \(L_\mu = e^{-\operatorname{Ent}(f)/n} (\det \operatorname{Cov}(\mu))^{1/(2n)}\) over all log-concave laws \(\mu\) on \(\mathbb{R}^n\), where \(f\) is the log-concave Lebesgue density of \(\mu\), \(\operatorname{Ent}(f)\) its differential entropy and \(\operatorname{Cov}(\mu)\) its covariance matrix. Here a log-concave law is a probability measure on \(\mathbb{R}^n\) with \(n \ge 1\), with finite second moments and with \(f \log f\) integrable, so for \(n = 0\) the supremum is over the empty family and is \(0\).

noncomputable def dimensionLawSupremum (n : ℕ) : ℝ≥0∞ :=
  ⨆ μ : LogConcaveLaw n, ENNReal.ofReal (lawIsotropicConstant μ)

Uses 2 · Used by 3

Statement usesLog-concave law · Isotropic constant of a log-concave law

Used byBody isotropic constants are bounded by the law supremum · The entropy isotropic constant is at most the full-dimensional supremum · Supremum of the isotropic constant over full-dimensional log-concave laws

DefinitionSupremum of isotropic constants of convex bodies#✓fully proved

This is the value \(\sup_{n \ge 1} \sup_K L_K \in [0, \infty]\), where for each dimension \(n \ge 1\) the inner supremum runs over all full-dimensional convex bodies \(K\) in \(\mathbb{R}^n\) and \(L_K\) is the isotropic constant of \(K\).

noncomputable def bodySupremum : ℝ≥0∞ :=
  ⨆ n : ℕ, ⨆ (_ : 0 < n), dimensionBodySupremum n

Sources

• constants/20b.md, the sharp-value body constant.

Uses 1 · Used by 1

Statement usesSupremum of isotropic constants in a fixed dimension

Used byCube lower bound for the supremal isotropic constant

DefinitionCentrally symmetric convex body#✓fully proved

For a natural number \(n\), a full-dimensional convex body \(K \subseteq \mathbb{R}^n\) is centrally symmetric when \(K = -K\), that is, for every \(x \in \mathbb{R}^n\), \(x \in K\) if and only if \(-x \in K\).

def IsCentrallySymmetric {n : ℕ} (K : FullDimensionalBody n) : Prop :=
  ∀ x : EuclideanSpace ℝ (Fin n),
    x ∈ (K.body : Set (EuclideanSpace ℝ (Fin n))) ↔
      -x ∈ (K.body : Set (EuclideanSpace ℝ (Fin n)))

Sources

• arXiv:2412.15044v1, Introduction after Theorem 1.2.

Uses 1 · Used by 1

Statement usesFull-dimensional convex body

Used bySupremum of isotropic constants of symmetric convex bodies

DefinitionSupremum of isotropic constants of symmetric convex bodies#✓fully proved

This is the value \(\sup_{n \ge 1} \sup_K L_K \in [0, \infty]\), where for each dimension \(n \ge 1\) the inner supremum runs over the full-dimensional convex bodies \(K\) in \(\mathbb{R}^n\) that are centrally symmetric, that is \(K = -K\), and \(L_K\) is the isotropic constant of \(K\).

noncomputable def centrallySymmetricBodySupremum : ℝ≥0∞ :=
  ⨆ n : ℕ, ⨆ (_ : 0 < n), ⨆ K : FullDimensionalBody n,
    ⨆ (_ : IsCentrallySymmetric K), ENNReal.ofReal (bodyIsotropicConstant K)

Uses 3

Statement usesFull-dimensional convex body · Centrally symmetric convex body · Isotropic constant of a convex body

DefinitionSquared-radius thin-shell width#✓fully proved

For a natural number \(n\), the squared-radius thin-shell width in dimension \(n\) is the supremum, in \([0, \infty]\), of \(\left(\int (|x|^2 - n)^2 \, d\mu(x) / n\right)^{1/2}\) (with \(0/0 = 0\)) over all isotropic log-concave probability measures \(\mu\) on \(\mathbb{R}^n\), that is, those with a log-concave Lebesgue density, mean zero and identity covariance.

It measures the fluctuation of the squared radius \(|x|^2\), not of the radius \(|x|\).

noncomputable def squaredRadiusThinShellWidth (n : ℕ) : ℝ≥0∞ :=
  ⨆ μ : Measure (EuclideanSpace ℝ (Fin n)), ⨆ (_ : ThinShell.IsIsotropicLogConcave μ),
    ENNReal.rpow (ThinShell.normalizedRadiusVariance μ) (1 / 2)

Uses 2

Statement usesIsotropic log-concave probability measures · Normalized radius variance

DefinitionSupremum of the isotropic constant over full-dimensional log-concave laws#✓fully proved

This is the supremum, in \([0, \infty]\), of the isotropic constant \(L_\mu = e^{-h(f)/n} (\det \mathrm{Cov}(\mu))^{1/(2n)}\) over all positive integers \(n\) and all log-concave laws \(\mu\) on \(\mathbb{R}^n\) with Lebesgue density \(f\), where \(h(f) = -\int_{\mathbb{R}^n} f \log f\) is the differential entropy of \(f\) and \(\mathrm{Cov}(\mu)\) is the covariance matrix of the coordinates under \(\mu\).

Each such law has a density on all of \(\mathbb{R}^n\), so laws supported on a proper affine subspace are not included here.

noncomputable def fullDimensionalLawSupremum : ℝ≥0∞ :=
  ⨆ n : ℕ, ⨆ (_ : 0 < n), dimensionLawSupremum n

Uses 1 · Used by 1

Statement usesSupremum of entropic isotropic constants in a fixed dimension

Used byThe entropy isotropic constant is at most the full-dimensional supremum

TheoremConstant densities on convex sets are log-concave#✓fully proved

Let \(K \subseteq \mathbb{R}^n\) be a measurable convex set and let \(c > 0\). Then the function equal to \(c\) on \(K\) and to \(0\) outside \(K\) is a log-concave density.

theorem isLogConcaveDensity_indicator_const {n : ℕ}
    {K : Set (EuclideanSpace ℝ (Fin n))} (hK : Convex ℝ K)
    (hm : MeasurableSet K) {c : ℝ} (hc : 0 < c) :
    IsLogConcaveDensity (K.indicator (fun _ => c))

Sources

• the uniform convex-body example in constants/20b.md.

Uses 1 · Used by 2

Statement usesLog-concave densities

Used byUniform law of a convex body · The uniform law on (−√3, √3) is isotropic log-concave

TheoremConditioning on a set is the normalized indicator density#✓fully proved

Let \(\mu\) be a measure on a measurable space \(\alpha\) and let \(K \subseteq \alpha\) be a measurable set with \(\mu(K) \neq 0\). Then the conditional measure \(\mu(\cdot \mid K)\), that is \(\mu(K)^{-1}\) times the restriction of \(\mu\) to \(K\), equals the measure with density \(x \mapsto \mu(K)^{-1} \mathbf{1}_K(x)\) with respect to \(\mu\). Here \(\mu(K)^{-1}\) is taken in \([0, \infty]\), so it is \(0\) when \(\mu(K) = \infty\).

theorem cond_eq_withDensity_indicator {α : Type*} [MeasurableSpace α]
    (μ : Measure α) {K : Set α} (hm : MeasurableSet K) (hK : μ K ≠ 0) :
    ProbabilityTheory.cond μ K =
      μ.withDensity (fun x => ENNReal.ofReal
        (K.indicator (fun _ => (μ K)⁻¹.toReal) x))

Sources

• constants/20b.md, normalized Lebesgue law on a convex body.

Used by 2

Used byUniform law of a convex body · The uniform law on (−√3, √3) is isotropic log-concave

DefinitionUniform density of a convex body#✓fully proved

Let \(n \ge 1\) and let \(K \subseteq \mathbb{R}^n\) be a full-dimensional convex body, so that its Lebesgue measure \(\mathrm{Vol}(K)\) is finite and positive. The uniform density of \(K\) is the function \(f_K \colon \mathbb{R}^n \to \mathbb{R}\) equal to \(1/\mathrm{Vol}(K)\) on \(K\) and to \(0\) outside \(K\).

noncomputable def bodyDensity {n : ℕ} (K : FullDimensionalBody n) :
    EuclideanSpace ℝ (Fin n) → ℝ :=
  (K.body : Set (EuclideanSpace ℝ (Fin n))).indicator
    (fun _ => (volume (K.body : Set (EuclideanSpace ℝ (Fin n))))⁻¹.toReal)

Uses 1 · Used by 2

Statement usesFull-dimensional convex body

Used byEntropy of the uniform density of a convex body · Uniform law of a convex body

DefinitionUniform law of a convex body#✓fully proved

Let \(n \ge 1\) and let \(K \subseteq \mathbb{R}^n\) be a full-dimensional convex body of Lebesgue measure \(\mathrm{Vol}(K)\). The uniform law of \(K\) is the log-concave law on \(\mathbb{R}^n\) whose probability measure is Lebesgue measure restricted to \(K\) and divided by \(\mathrm{Vol}(K)\), and whose density is the uniform density of \(K\).

noncomputable def bodyLogConcaveLaw {n : ℕ} (K : FullDimensionalBody n) : LogConcaveLaw n where
  dimension_pos := K.dimension_pos
  law := bodyLaw K
  probability := bodyLaw_probability K
  density := bodyDensity K
  logConcave := bodyDensity_logConcave K
  law_eq := bodyLaw_eq_withDensity K
  moment_one := bodyLaw_integrable_coord K
  moment_two := bodyLaw_integrable_coord_mul K
  entropy_integrable := bodyDensity_entropy_integrable K

Uses 7 · Used by 3

Statement usesFull-dimensional convex body · Log-concave law · Uniform density of a convex body · Uniform distribution on a convex body · Log-concave densities · Conditioning on a set is the normalized indicator density · Constant densities on convex sets are log-concave

Used byThe uniform law on a convex body as an intrinsic log-concave law · The entropy and volume isotropic constants of a convex body agree · Body isotropic constants are bounded by the law supremum

TheoremEntropy of the uniform density of a convex body#✓fully proved

Let \(n \ge 1\) and let \(K \subseteq \mathbb{R}^n\) be a full-dimensional convex body with Lebesgue measure \(\mathrm{Vol}(K)\) and uniform density \(f_K\), equal to \(1/\mathrm{Vol}(K)\) on \(K\) and to \(0\) outside \(K\). Then the differential entropy \(-\int_{\mathbb{R}^n} f_K(x) \log f_K(x) \, dx\) of \(f_K\) equals \(\log \mathrm{Vol}(K)\).

theorem bodyDensity_entropy {n : ℕ} (K : FullDimensionalBody n) :
    differentialEntropy (bodyDensity K) =
      Real.log (volume (K.body : Set (EuclideanSpace ℝ (Fin n)))).toReal

Uses 3 · Used by 1

Statement usesFull-dimensional convex body · Uniform density of a convex body · Differential entropy

Used byThe entropy and volume isotropic constants of a convex body agree

TheoremThe entropy and volume isotropic constants of a convex body agree#✓fully proved

Let \(n \ge 1\) and let \(K \subseteq \mathbb{R}^n\) be a full-dimensional convex body of Lebesgue measure \(\mathrm{Vol}(K)\), with uniform probability measure \(\lambda_K\), uniform density \(f_K\), and covariance matrix \(C_K\) of the coordinates under \(\lambda_K\). Then the entropy isotropic constant of the uniform law of \(K\) equals the isotropic constant of \(K\), that is, \(\exp\big(\frac{1}{n} \int_{\mathbb{R}^n} f_K(x) \log f_K(x) \, dx\big) (\det C_K)^{1/(2n)} = \big(\det C_K / \mathrm{Vol}(K)^2\big)^{1/(2n)}\).

theorem bodyLogConcaveLaw_isotropicConstant {n : ℕ} (K : FullDimensionalBody n) :
    lawIsotropicConstant (bodyLogConcaveLaw K) = bodyIsotropicConstant K

Uses 10 · Used by 1

Statement usesFull-dimensional convex body · Isotropic constant of a convex body · Uniform law of a convex body · Isotropic constant of a log-concave law

Proof usesLog-concave law · Entropy of the uniform density of a convex body · Uniform distribution on a convex body · Covariance matrix · Covariance matrices of log-concave laws are positive semidefinite · Differential entropy

Used byBody isotropic constants are bounded by the law supremum

TheoremBody isotropic constants are bounded by the law supremum#✓fully proved

For every \(n \in \mathbb{N}\), the supremum of the isotropic constants of full-dimensional convex bodies in \(\mathbb{R}^n\) is at most the supremum of the entropy isotropic constants of probability laws on \(\mathbb{R}^n\) with a log-concave Lebesgue density \(f\) such that every coordinate \(x_i\) and every product \(x_i x_j\) is integrable under the law and \(f \log f\) is Lebesgue integrable, both suprema taken in \([0, \infty]\). Both families are defined only for \(n \ge 1\), so for \(n = 0\) they are empty and both suprema are \(0\).

theorem dimensionBodySupremum_le_lawSupremum (n : ℕ) :
    dimensionBodySupremum n ≤ dimensionLawSupremum n

Uses 8

Statement usesSupremum of isotropic constants in a fixed dimension · Supremum of entropic isotropic constants in a fixed dimension

Proof usesFull-dimensional convex body · Log-concave law · Isotropic constant of a convex body · Uniform law of a convex body · The entropy and volume isotropic constants of a convex body agree · Isotropic constant of a log-concave law

StructureLog-concave law in intrinsic coordinates#✓fully proved

Fix an ambient dimension \(N\). An intrinsic log-concave law on \(\mathbb{R}^N\) consists of a dimension \(d\), a log-concave law \(\nu\) on \(\mathbb{R}^d\) (that is, \(d > 0\) and \(\nu\) is a probability measure with a log-concave Lebesgue density \(f\), integrable coordinates and coordinate products, and integrable \(f \log f\)), an affine isometric embedding \(\varphi : \mathbb{R}^d \to \mathbb{R}^N\) of Euclidean spaces, and a measure \(\mu\) on \(\mathbb{R}^N\), such that \(\mu\) is the pushforward \(\varphi_* \nu\) and the image of \(\varphi\) equals the affine span of the support of \(\mu\).

The pushforward identity ties the ambient law \(\mu\) to the density and entropy of \(\nu\), which are computed in the intrinsic coordinates.

structure IntrinsicLogConcaveLaw (ambient : ℕ) where
  dimension : ℕ
  coordinates : LogConcaveLaw dimension
  chart : EuclideanSpace ℝ (Fin dimension) →ᵃⁱ[ℝ] EuclideanSpace ℝ (Fin ambient)
  law : Measure (EuclideanSpace ℝ (Fin ambient))
  law_eq : law = coordinates.law.map chart
  span_eq : Set.range chart =
    (affineSpan ℝ law.support : Set (EuclideanSpace ℝ (Fin ambient)))

Uses 1 · Used by 4

Statement usesLog-concave law

Used byThe uniform law on a convex body as an intrinsic log-concave law · Supremum of intrinsic isotropic constants in a fixed ambient dimension · The entropy isotropic constant is at most the full-dimensional supremum · Isotropic constant of an intrinsic log-concave law

DefinitionIsotropic constant of an intrinsic log-concave law#✓fully proved

Let \(\mu\) be an intrinsic log-concave law on \(\mathbb{R}^N\), given by a log-concave law \(\nu\) on \(\mathbb{R}^d\) with density \(f\) and an affine isometric embedding of \(\mathbb{R}^d\) onto the affine span of the support of \(\mu\). The isotropic constant of \(\mu\) is the entropy isotropic constant of \(\nu\),

\[L_\mu = e^{-h(f)/d} \, \det(\operatorname{Cov} \nu)^{1/(2d)},\]

where \(h(f) = -\int_{\mathbb{R}^d} f \log f\) is the differential entropy of \(f\) and \(\operatorname{Cov} \nu\) is the covariance matrix of the coordinates under \(\nu\).

Entropy and covariance are thus computed relative to the intrinsic affine span.

noncomputable def intrinsicLawIsotropicConstant {ambient : ℕ}
    (μ : IntrinsicLogConcaveLaw ambient) : ℝ :=
  lawIsotropicConstant μ.coordinates

Uses 3 · Used by 2

Statement usesLog-concave law in intrinsic coordinates · Log-concave law · Isotropic constant of a log-concave law

Used bySupremum of intrinsic isotropic constants in a fixed ambient dimension · The entropy isotropic constant is at most the full-dimensional supremum

DefinitionSupremum of intrinsic isotropic constants in a fixed ambient dimension#✓fully proved

For a natural number \(N\), this is the supremum in \([0, \infty]\) of the isotropic constants \(L_\mu\) over all intrinsic log-concave laws \(\mu\) on \(\mathbb{R}^N\).

The family includes laws whose support spans a proper affine subspace of positive dimension.

noncomputable def dimensionIntrinsicLawSupremum (ambient : ℕ) : ℝ≥0∞ :=
  ⨆ μ : IntrinsicLogConcaveLaw ambient, ENNReal.ofReal (intrinsicLawIsotropicConstant μ)

Uses 2 · Used by 2

Statement usesLog-concave law in intrinsic coordinates · Isotropic constant of an intrinsic log-concave law

Used byEntropy-convention isotropic constant · The entropy isotropic constant is at most the full-dimensional supremum

DefinitionEntropy-convention isotropic constant#✓fully proved

This is the supremum, in \([0, \infty]\), over all dimensions \(N > 0\) of the supremum of the isotropic constants \(L_\mu\) over all intrinsic log-concave laws \(\mu\) on \(\mathbb{R}^N\). A law supported on a proper affine subspace thus contributes the isotropic constant computed in orthonormal coordinates on its affine span.

noncomputable def entropyIsotropicConstant : ℝ≥0∞ :=
  ⨆ n : ℕ, ⨆ (_ : 0 < n), dimensionIntrinsicLawSupremum n

Sources

• C20b, with the entropy convention and actual intrinsic-span laws.

Uses 1 · Used by 1

Statement usesSupremum of intrinsic isotropic constants in a fixed ambient dimension

Used byThe entropy isotropic constant is at most the full-dimensional supremum

TheoremThe entropy isotropic constant is at most the full-dimensional supremum#✓fully proved

The entropy isotropic constant, the supremum of the isotropic constants of intrinsic log-concave laws over all ambient dimensions \(N > 0\), is at most the supremum in \([0, \infty]\), over all dimensions \(n > 0\) and all log-concave laws \(\nu\) on \(\mathbb{R}^n\), of the entropy isotropic constant \(L_\nu = e^{-h(f)/n} \det(\operatorname{Cov} \nu)^{1/(2n)}\), where \(f\) is the density of \(\nu\) and \(h(f) = -\int f \log f\).

Each intrinsic law contributes the isotropic constant of its coordinate law, which is a full-dimensional log-concave law.

theorem entropyIsotropicConstant_le_fullDimensionalSupremum :
    entropyIsotropicConstant ≤ fullDimensionalLawSupremum

Uses 8

Statement usesEntropy-convention isotropic constant · Supremum of the isotropic constant over full-dimensional log-concave laws

Proof usesLog-concave law in intrinsic coordinates · Log-concave law · Supremum of intrinsic isotropic constants in a fixed ambient dimension · Supremum of entropic isotropic constants in a fixed dimension · Isotropic constant of an intrinsic log-concave law · Isotropic constant of a log-concave law

TheoremThe uniform law on a convex body spans the whole space#✓fully proved

For a full-dimensional convex body \(K \subseteq \mathbb{R}^n\) (a convex body with nonempty interior, \(n > 0\)), the affine span of the support of the uniform probability law on \(K\) is all of \(\mathbb{R}^n\).

theorem bodyLaw_affineSpan_support {n : ℕ} (K : FullDimensionalBody n) :
    affineSpan ℝ (bodyLaw K).support = ⊤

Uses 2 · Used by 1

Statement usesFull-dimensional convex body · Uniform distribution on a convex body

Used byThe uniform law on a convex body as an intrinsic log-concave law

DefinitionThe uniform law on a convex body as an intrinsic log-concave law#✓fully proved

For a full-dimensional convex body \(K \subseteq \mathbb{R}^n\), this is the intrinsic log-concave law on \(\mathbb{R}^n\) of intrinsic dimension \(n\) whose chart is the identity map of \(\mathbb{R}^n\), whose law is the uniform probability law on \(K\), and whose coordinate law is that uniform law viewed as a log-concave law with density \(\mathbf{1}_K / \operatorname{vol}(K)\).

noncomputable def bodyIntrinsicLogConcaveLaw {n : ℕ} (K : FullDimensionalBody n) :
    IntrinsicLogConcaveLaw n where
  dimension := n
  coordinates := bodyLogConcaveLaw K
  chart := AffineIsometry.id
  law := bodyLaw K
  law_eq := by simp [bodyLogConcaveLaw]
  span_eq := by simp [bodyLaw_affineSpan_support K]

Uses 6

Statement usesFull-dimensional convex body · Log-concave law in intrinsic coordinates · Log-concave law · Uniform distribution on a convex body · The uniform law on a convex body spans the whole space · Uniform law of a convex body

DefinitionIdentification of the line with one-dimensional Euclidean space#✓fully proved

The linear isometric isomorphism from \(\mathbb{R}\) onto one-dimensional Euclidean space \(\mathbb{R}^1\) that sends a real number \(x\) to the vector whose only coordinate is \(x\).

noncomputable def lineIsometry : ℝ ≃ₗᵢ[ℝ] EuclideanSpace ℝ (Fin 1) :=
  (OrthonormalBasis.singleton (Fin 1) ℝ).repr

Used by 6

Used bySymmetric interval as a convex body · Cube lower bound for the supremal isotropic constant · Symmetric interval in one-dimensional Euclidean space · The uniform law on (−1, 1) is not isotropic log-concave · The uniform law on (−√3, √3) is isotropic log-concave · Membership in the unit interval body

DefinitionSymmetric interval in one-dimensional Euclidean space#✓fully proved

For a real number \(a\), the set of points of one-dimensional Euclidean space \(\mathbb{R}^1\) whose only coordinate lies in the closed interval \([-a, a]\). It is empty when \(a < 0\).

def symmetricInterval (a : ℝ) : Set (EuclideanSpace ℝ (Fin 1)) :=
  lineIsometry.symm ⁻¹' Set.Icc (-a) a

Uses 1 · Used by 5

Statement usesIdentification of the line with one-dimensional Euclidean space

Used bySymmetric interval as a convex body · Cube lower bound for the supremal isotropic constant · Uniform distribution on a symmetric interval · The uniform law on (−1, 1) is not isotropic log-concave · The uniform law on (−√3, √3) is isotropic log-concave

DefinitionUniform distribution on a symmetric interval#✓fully proved

For a real number \(a\), the measure on one-dimensional Euclidean space \(\mathbb{R}^1\) obtained by conditioning Lebesgue measure on the set \(\{x : -a \le x_1 \le a\}\) of points whose only coordinate \(x_1\) lies in \([-a, a]\), that is, Lebesgue measure restricted to this set and divided by its measure. For \(a > 0\) this is the uniform probability distribution with density \(1/(2a)\) on the interval; for \(a \le 0\) the set has measure zero and the conditioned measure is the zero measure.

It is conditioned Lebesgue measure, not a discrete uniform measure.

noncomputable def uniformInterval (a : ℝ) : Measure (EuclideanSpace ℝ (Fin 1)) :=
  ProbabilityTheory.cond volume (symmetricInterval a)

Uses 1 · Used by 5

Statement usesSymmetric interval in one-dimensional Euclidean space

Used byCube lower bound for the supremal isotropic constant · The uniform law on (−1, 1) is not isotropic log-concave · Radius fluctuation of the uniform law on (−√3, √3) · The uniform law on (−√3, √3) is isotropic log-concave · Thin-shell variance bound for the uniform law on (−√3, √3)

TheoremThe uniform law on (−√3, √3) is isotropic log-concave#✓fully proved

The uniform distribution on the symmetric interval \([-\sqrt{3}, \sqrt{3}]\) of one-dimensional Euclidean space \(\mathbb{R}^1\) is an isotropic log-concave probability measure: it has a log-concave density with respect to Lebesgue measure, mean zero and identity covariance.

theorem uniformInterval_sqrt_three_isIsotropicLogConcave :
    IsIsotropicLogConcave (uniformInterval (Real.sqrt 3))

Sources

• the one-dimensional isotropic cube, uniform on [-√3, √3].

Uses 7 · Used by 2

Statement usesIsotropic log-concave probability measures · Uniform distribution on a symmetric interval

Proof usesLog-concave densities · Conditioning on a set is the normalized indicator density · Constant densities on convex sets are log-concave · Identification of the line with one-dimensional Euclidean space · Symmetric interval in one-dimensional Euclidean space

Used byRadius fluctuation of the uniform law on (−√3, √3) · Thin-shell variance bound for the uniform law on (−√3, √3)

TheoremThin-shell variance bound for the uniform law on (−√3, √3)#✓fully proved

Let \(\mu\) be the uniform distribution on the symmetric interval \([-\sqrt{3}, \sqrt{3}]\) of one-dimensional Euclidean space \(\mathbb{R}^1\). Its normalized radius variance \(\int (\|x\|^2 - 1)^2 \, d\mu(x)\) is at most the thin-shell variance constant, the supremum of the normalized radius variance over all isotropic log-concave probability measures in all positive dimensions.

theorem uniformInterval_variance_le_thinShellConstant :
    normalizedRadiusVariance (uniformInterval (Real.sqrt 3)) ≤ thinShellVarianceConstant

Uses 5

Statement usesNormalized radius variance · Thin-shell variance constant · Uniform distribution on a symmetric interval

Proof usesThe thin-shell variance constant bounds the normalized radius variance of isotropic log-concave measures · The uniform law on (−√3, √3) is isotropic log-concave

TheoremRadius fluctuation of the uniform law on (−√3, √3)#✓fully proved

Let \(\mu\) be the uniform distribution on the symmetric interval \([-\sqrt{3}, \sqrt{3}]\) of one-dimensional Euclidean space \(\mathbb{R}^1\). Then \(\int (\|x\| - \sqrt{1})^2 \, d\mu(x)\), the mean squared deviation of the Euclidean norm from \(\sqrt{1} = 1\), is at most the thin-shell variance constant.

theorem uniformInterval_radiusFluctuation_le_thinShellConstant :
    (∫⁻ x, ENNReal.ofReal ((‖x‖ - Real.sqrt (1 : ℝ)) ^ 2)
      ∂uniformInterval (Real.sqrt 3)) ≤ thinShellVarianceConstant

Uses 4

Statement usesThin-shell variance constant · Uniform distribution on a symmetric interval

Proof usesThe thin-shell variance constant bounds the radius fluctuation · The uniform law on (−√3, √3) is isotropic log-concave

TheoremThe uniform law on (−1, 1) is not isotropic log-concave#✓fully proved

The uniform distribution on the symmetric interval \([-1, 1]\) of one-dimensional Euclidean space \(\mathbb{R}^1\) is not an isotropic log-concave probability measure.

Its second moment is \(1/3\) rather than \(1\).

theorem uniformInterval_one_not_isIsotropicLogConcave :
    ¬ IsIsotropicLogConcave (uniformInterval 1)

Uses 5

Statement usesIsotropic log-concave probability measures · Uniform distribution on a symmetric interval

Proof usesLog-concave densities · Identification of the line with one-dimensional Euclidean space · Symmetric interval in one-dimensional Euclidean space

DefinitionSymmetric interval as a convex body#✓fully proved

For a real number \(a > 0\), this is the closed interval \([-a, a]\) in the one-dimensional Euclidean space, regarded as a full-dimensional convex body.

MathlibExt.Probability.IsotropicConstant.intervalBody · 22 lines

noncomputable def intervalBody (a : ℝ) (ha : 0 < a) : FullDimensionalBody 1 where
  body := {
    carrier := symmetricInterval a
    convex' := symmetricInterval_convex a
    isCompact' := by
      convert (isCompact_Icc : IsCompact (Set.Icc (-a) a)).image
        lineIsometry.continuous using 1
      ext x
      constructor
      · intro hx
        exact ⟨lineIsometry.symm x, hx, by simp⟩
      · rintro ⟨y, hy, rfl⟩
        simpa [symmetricInterval] using hy
    nonempty' := ⟨lineIsometry 0, by simp [symmetricInterval, ha.le]⟩
  }
  dimension_pos := by decide
  interior_nonempty := by
    have hopen : IsOpen (lineIsometry.symm ⁻¹' Set.Ioo (-a) a) :=
      isOpen_Ioo.preimage lineIsometry.symm.continuous
    have hsub : lineIsometry.symm ⁻¹' Set.Ioo (-a) a ⊆ symmetricInterval a :=
      Set.preimage_mono Set.Ioo_subset_Icc_self
    exact ⟨lineIsometry 0, interior_maximal hsub hopen (by simp [ha])⟩

Uses 3 · Used by 1

Statement usesFull-dimensional convex body · Identification of the line with one-dimensional Euclidean space · Symmetric interval in one-dimensional Euclidean space

Used byUnit interval body

DefinitionUnit interval body#✓fully proved

The unit interval body is the closed interval \([-1/2, 1/2]\), of length one and centred at the origin, in the one-dimensional Euclidean space, regarded as a full-dimensional convex body.

noncomputable def unitIntervalBody : FullDimensionalBody 1 :=
  intervalBody (1 / 2) (by norm_num)

Uses 2 · Used by 2

Statement usesFull-dimensional convex body · Symmetric interval as a convex body

Used byCube lower bound for the supremal isotropic constant · Membership in the unit interval body

TheoremCube lower bound for the supremal isotropic constant#✓fully proved

The supremum, over all positive integers \(n\) and all full-dimensional convex bodies \(K \subseteq \mathbb{R}^n\), of the isotropic constant \(L_K = \left(\det \mathrm{Cov}(K) / \mathrm{Vol}(K)^2\right)^{1/(2n)}\), where \(\mathrm{Cov}(K)\) is the covariance matrix of the uniform distribution on \(K\), is at least \(1/\sqrt{12}\).

The interval \([-1/2, 1/2]\) in dimension one already attains \(L_K = 1/\sqrt{12}\).

theorem inv_sqrt_twelve_le_bodySupremum :
    ENNReal.ofReal (1 / Real.sqrt 12) ≤ bodySupremum

Uses 10

Statement usesSupremum of isotropic constants of convex bodies

Proof usesFull-dimensional convex body · Isotropic constant of a convex body · Uniform distribution on a convex body · Covariance matrix · Supremum of isotropic constants in a fixed dimension · Unit interval body · Identification of the line with one-dimensional Euclidean space · Symmetric interval in one-dimensional Euclidean space · Uniform distribution on a symmetric interval

TheoremMembership in the unit interval body#✓fully proved

A point \(x\) of the one-dimensional Euclidean space lies in the unit interval body if and only if its single coordinate \(x_1\) satisfies \(-1/2 \le x_1 \le 1/2\).

theorem unitIntervalBody_mem_iff (x : EuclideanSpace ℝ (Fin 1)) :
    x ∈ (unitIntervalBody.body : Set (EuclideanSpace ℝ (Fin 1))) ↔
      ∀ i : Fin 1, -(1 / 2 : ℝ) ≤ x i ∧ x i ≤ (1 / 2 : ℝ)

Uses 3

Statement usesFull-dimensional convex body · Unit interval body

Proof usesIdentification of the line with one-dimensional Euclidean space

41 fully proved

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.