Samplinglib
Lean gate not recorded for this source state main · 9bb7a7394ab0

Bench / sampling

sogb-008 · public-dev · editorial and formal status separate

A log-concave shape is not yet a probability density

Log-Concave Sampling · natural-language: L1 (author-assigned; calibration pending)

Why this difficulty?

Identify the positive shape, logarithm, reference measure and normalizing constant; no tail-integrability proof is requested.

Editorial review and exact formal-coverage boundary

AI editorial review accepted. This is not canonical theorem publication, full Lean coverage or empirical difficulty calibration.

  • This QA has no aligned Lean view. Borel measurability bookkeeping, the numerical normalization criterion and its probability-density verification, positivity of the Lebesgue integral, and the infinite-volume V=0 example are independently checked prose obligations beyond the cited log-concavity leaf.

Content-bound review status and evidence hashes · Independent reports and frozen inputs. Historical rejected wording is audit material, not training gold.

Assumptions and conventions

  • On \(\mathbb{R}^{d}\) with \(d\ge 1\) and Lebesgue reference measure, V is a finite real-valued Borel measurable convex function. Set \(ρ(x)=exp(-V(x))\).

Natural-language question

Identify the log-concave shape and its logarithm. What additional numerical condition on \(Z=\int ρ(x)dx\) is required before \(ρ/Z\) defines a probability density? State which reference measure the word density refers to.

Reference mathematical proof

  1. The shape \(ρ\) is strictly positive and Borel measurable. Its logarithm is \(-V\), a concave function by convexity of V, so this is a positive log-concave shape.

  2. The normalizing quantity is \[Z=\int_{\mathbb R^d}e^{-V(x)}\,dx.\] A probability normalization requires \(0<Z<\infty \), after which \(p(x)=ρ(x)/Z\) integrates to one against Lebesgue measure.

  3. Log-concavity of the shape is a pointwise convex-analysis property; the finite integral is a separate analytic condition. This question asks to identify that obligation, not to prove that it holds for every convex potential.

  4. For example \(V=0\) has the log-concave shape \(ρ=1\) but infinite Lebesgue integral on \(\mathbb{R}^{d}\). Thus the shape alone is not a normalized sampling target.

Formal support and missing Lean alignment

The existing declaration supports the positive log-concavity claim only. This full definition/normalization QA has no aligned Lean view.

Assessment rubric · 4 points
  1. Identifies \(ρ=exp(-V)>0\) and log \(ρ=-V\). (1 point)
  2. Relates concavity of log \(ρ\) to convexity of V. (1 point)
  3. States \(0<Z<\infty \) and \(p=ρ/Z\) rather than treating shape as already normalized. (1 point)
  4. Names Lebesgue reference measure and keeps integrability separate from shape. (1 point)

Lean view: not yet aligned

The existing declaration supports the positive log-concavity claim only. This full definition/normalization QA has no aligned Lean view.

This support theorem does not certify the complete QA or its explanatory counterexamples.

What this does—and does not—verify

No Gibbs normalization or tail-integrability theorem is supplied by the log-concavity leaf.

Existing library mathematics reused; no new mathematical leaf or paper-completion credit. The editorial panel records the exact current review scope and remaining unformalized explanation.

Sources, graph location and dependencies

Original introductory exercise over the local positive log-concavity API; no textbook prose is reproduced.

Exact local source and full context · Locate the owning module (declaration not yet indexed in this graph)

AutoSamplingTheory.TechnicalLemmas.Geometry.LogConcavity.logConcaveOn_exp_neg_of_convexOn

ASTIS formal support (not an equivalent QA)

    Mathlib facts / definitions

      Binding SHA-256: ae0a2d0d8f65fbe39a5c2ed55cbe7b93bde710026ec00ed08132abeedefb2794