Samplinglib
Lean gate not recorded for this source state main · 0e31a3cda412
ASTIS mathematical exposition

Log-concavity with the explicit Laplace prefactor

AutoSamplingTheory.TechnicalLemmas.Geometry.LogConcavity.logConcaveOn_explicit_abs_linear_normalized_density · theorem · Teaching coverage

Statement

Let the ambient space be ℝ; let a,b∈ℝ with a>0. Put V=a|x|+b and Z=2 exp(−b)/a. Then the explicitly scaled function Z⁻¹ exp(−V) is positive log-concave on ℝ. The theorem proves only this shape property; despite the existing declaration's name, it supplies no equality between Z and an integral.

\[Z=\frac{2e^{-b}}a,\qquad V=a|x|+b,\qquad a>0\Longrightarrow\operatorname{LC}_{ℝ}(Z^{-1}e^{-V}).\]

All objects and hypotheses

  • The ambient scalar field and state space are ℝ with their usual additive/module structures.
  • a,b : ℝ; ha : 0<a, with b arbitrary.
  • {'term': 'Positive log-concavity', 'text': 'LC_s(f) means strict positivity of f at every point of s and concavity of log f on the convex domain s. No zero-valued points are included in this convention.', 'formula': '\\operatorname{LC}_s(f)\\iff(\\forall x\\in s,\\ f(x)>0)\\land\\operatorname{Concave}_s(\\log f).'}
  • {'term': 'Convex combinations and Jensen inequalities', 'text': 'Throughout, x,y lie in the stated domain; λ,θ are nonnegative real weights with λ+θ=1. The Lean code often names these weights a,b, independently of the a,b coefficients in specialized potentials.', 'formula': 'z=\\lambda x+\\theta y,\\quad \\lambda,\\theta\\ge0,\\quad\\lambda+\\theta=1;\\qquad V(z)\\le\\lambda V(x)+\\theta V(y)\\text{ for convex }V.'}
  • {'term': 'Geometry, not probability normalization', 'text': 'The module proves shapes and convexity properties of real-valued functions. It has no reference measure in its declarations. In particular, names containing normalized_density do not themselves prove normalization, and the quadratic prefactor is not certified as the integral of an arbitrary norm-based shape.', 'formula': '\\operatorname{LC}(Z^{-1}e^{-V})\\quad\\text{does not assert}\\quad Z=\\int e^{-V}\\,d\\mu\\quad\\text{or}\\quad \\int Z^{-1}e^{-V}\\,d\\mu=1.'}

Mathematical proof

1. Show the displayed scale is positive

The exponential e⁻ᵇ is positive, 2 is positive, and the denominator a is positive by hypothesis. Hence Z=2e⁻ᵇ/a is strictly positive. The source's positivity step proves this elementary sign statement, not an integral evaluation.

\[2>0,\ e^{-b}>0,\ a>0\Longrightarrow Z=\frac{2e^{-b}}a>0.\]
Corresponding Lean step

have hZpos : 0 < 2 * Real.exp (-b) / a := by positivity

hZpos names a proved strict-positivity fact for the displayed scale; it is not an integral formula.

2. The reciprocal is a positive multiplier

A strictly positive real number has a strictly positive reciprocal. Also a>0 implies a≥0, so the hypotheses of the already-proved rescaled-shape theorem are satisfied.

\[Z>0\Longrightarrow Z^{-1}>0,\qquad a>0\Longrightarrow a\ge0.\]
Corresponding Lean step
ha.le
(inv_pos.mpr hZpos)

hZpos names a proved strict-positivity fact for the displayed scale; it is not an integral formula.

3. Specialize the positive-rescaling theorem

Use the existing result for the same potential V with multiplier c=Z⁻¹. That result gives exactly the requested log-concavity. No extra property of this numerical choice of Z is used beyond its positivity.

\[\operatorname{LC}_{ℝ}(ce^{-V}),\quad c=Z^{-1}\Longrightarrow\operatorname{LC}_{ℝ}(Z^{-1}e^{-V}).\]
Corresponding Lean step
exact logConcaveOn_const_mul_exp_neg_abs_linear
  (a := a) (b := b) (c := (2 * Real.exp (-b) / a)⁻¹) ha.le
  (inv_pos.mpr hZpos)

hZpos names a proved strict-positivity fact for the displayed scale; it is not an integral formula.

Lean statement · logConcaveOn_explicit_abs_linear_normalized_density

Braces name inputs Lean can infer, and bracketed classes state the ambient structures listed above. The assumptions before the final colon are inputs; the expression after it is the exact property this declaration establishes. hZpos is only a positivity proof for a displayed real expression. inv_pos supplies positivity of its reciprocal. The final existing theorem accepts every positive multiplier, so the name normalized_density must not be read as a proof that the function integrates to one.

Braces mark parameters Lean can infer; square brackets request structures such as a measurable space or probability measure. Named hypotheses are mathematical premises, not facts established by this declaration. Section parameters are described in the mathematical hypotheses above; the module link retains their exact source context.

theorem logConcaveOn_explicit_abs_linear_normalized_density {a b : ℝ} (ha : 0 < a) :
    LogConcavity.LogConcaveOn (Set.univ : Set ℝ)
      (fun x : ℝ => (2 * Real.exp (-b) / a)⁻¹ * Real.exp (-(a * |x| + b)))

Exact module and namespace context

Lean proof · logConcaveOn_explicit_abs_linear_normalized_density

hZpos is only a positivity proof for a displayed real expression. inv_pos supplies positivity of its reciprocal. The final existing theorem accepts every positive multiplier, so the name normalized_density must not be read as a proof that the function integrates to one.

Braces mark parameters Lean can infer; square brackets request structures such as a measurable space or probability measure. Named hypotheses are mathematical premises, not facts established by this declaration. Section parameters are described in the mathematical hypotheses above; the module link retains their exact source context.

theorem logConcaveOn_explicit_abs_linear_normalized_density {a b : ℝ} (ha : 0 < a) :
    LogConcavity.LogConcaveOn (Set.univ : Set ℝ)
      (fun x : ℝ => (2 * Real.exp (-b) / a)⁻¹ * Real.exp (-(a * |x| + b))) := by
  have hZpos : 0 < 2 * Real.exp (-b) / a := by
    positivity
  exact logConcaveOn_const_mul_exp_neg_abs_linear
    (a := a) (b := b) (c := (2 * Real.exp (-b) / a)⁻¹) ha.le
    (inv_pos.mpr hZpos)

/-- The squared norm is convex on any real normed vector space. -/

Exact module and namespace context

Scope and omitted-condition boundaries

  • No measure, integral, total mass, or normalized-probability conclusion appears in the actual Lean statement.
  • The classical Laplace normalizing integral is a separate result, not used or proved by this declaration.
  • This documentation adds no Lean theorem, compilation evidence, source-equivalence verdict, or new source-fidelity certification.

Source and reuse

ASTIS parents called

Mathlib API called (external library)

  • Real.exp_pos
  • inv_pos

Mathematical sources

ASTIS prose is not a quotation or a source-equivalence certificate. Definitions and aliases are explained as constructions, not counted as new mathematical proofs.