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

The identity function is log-concave on the positive ray

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

Statement

The function f(x)=x is positive log-concave on the open positive ray (0,∞) in ℝ.

\[\operatorname{LC}_{(0,\infty)}(x\mapsto x),\qquad a\log x+b\log y\le\log(ax+by)\quad(x,y>0,\ a,b\ge0,\ a+b=1).\]

All objects and hypotheses

  • The ambient scalar field and state space are ℝ with their usual additive/module structures.
  • The ambient module is ℝ and the domain is Set.Ioi (0 : ℝ); there are no additional parameters.
  • {'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. Read positivity from domain membership

Membership in the open ray means exactly x>0. Since f(x)=x, this is the required positivity.

\[x\in(0,\infty)\Longrightarrow f(x)=x>0.\]
Corresponding Lean step

fun _ hx => hx

The identifiers refer to the assumptions or previously proved facts described in this step; the full original proof below supplies their exact context.

2. Reuse the concavity of the real logarithm

Mathlib proves that log is strictly concave on (0,∞). Its weaker concavity statement therefore gives the required logarithmic concavity of f; pair it with positivity.

\[\log\text{ strictly concave on }(0,\infty)\Longrightarrow\log f=\log\text{ concave on }(0,\infty).\]
Corresponding Lean step

⟨fun _ hx => hx, strictConcaveOn_log_Ioi.concaveOn⟩

The identifiers refer to the assumptions or previously proved facts described in this step; the full original proof below supplies their exact context.

Lean statement · logConcaveOn_id_Ioi

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. Ioi 0 is the set of reals greater than zero. .concaveOn forgets strictness in the imported strict-concavity theorem. The result is a function-shape example, not a probability density on the unbounded ray.

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_id_Ioi :
    LogConcaveOn (Ioi (0 : ℝ)) (fun x : ℝ => x)

Exact module and namespace context

Lean proof · logConcaveOn_id_Ioi

Ioi 0 is the set of reals greater than zero. .concaveOn forgets strictness in the imported strict-concavity theorem. The result is a function-shape example, not a probability density on the unbounded ray.

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_id_Ioi :
    LogConcaveOn (Ioi (0 : ℝ)) (fun x : ℝ => x) :=
  ⟨fun _ hx => hx, strictConcaveOn_log_Ioi.concaveOn⟩

end LogConcavity
end Geometry
end TechnicalLemmas
end AutoSamplingTheory

Exact module and namespace context

Scope and omitted-condition boundaries

  • No integrability, finite mass or normalization on (0,∞).
  • 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)

  • strictConcaveOn_log_Ioi
  • StrictConcaveOn.concaveOn

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.