LogConcavity: mathematical reading route

Read the statements and derivations in source order. Every result has its own optional Lean statement and proof. Source assumptions, library reuse and unproved boundaries are kept explicit.

Positive log-concavity on a domain
Unpack the definition of positive log-concavity
Build a log-concavity proof from its two ingredients
A positive log-concave function is positive at each domain point
Read the concavity of the logarithm
The negative logarithm is a convex potential
Sublevel sets of the negative-log potential are convex
The log-concavity domain is convex
Every superlevel set of a positive log-concave function is convex
Positive log-concavity implies quasiconcavity
Restrict to a convex smaller domain
Restrict log-concavity to a superlevel set
Log-concavity survives linear precomposition
Log-concavity survives affine precomposition
Products on a common domain preserve positive log-concavity
Nonnegative real powers preserve positive log-concavity
Tensor products are log-concave on product domains
Positive rescaling preserves log-concavity
Positive constants are log-concave on convex domains
A convex potential gives a log-concave Gibbs shape
A positively rescaled convex-potential Gibbs shape is log-concave
Absolute value is convex on the real line
Convexity of a absolute-linear potential
Log-concavity of a absolute-linear Gibbs shape
Positive rescaling of the absolute-linear Gibbs shape
Log-concavity with the explicit Laplace prefactor
Squared norms are convex on real normed spaces
Convexity of a quadratic-norm potential
Log-concavity of a quadratic-norm Gibbs shape
Positive rescaling of the quadratic-norm Gibbs shape
Log-concavity with the explicit quadratic prefactor
Convexity of a shifted quadratic-norm potential
Log-concavity of a shifted quadratic-norm Gibbs shape
Positive rescaling of the shifted quadratic-norm Gibbs shape
Log-concavity with the explicit quadratic prefactor after translation
Convexity of a two-point difference-quadratic potential
Log-concavity of a two-point difference-quadratic Gibbs shape
Positive rescaling of the two-point difference-quadratic Gibbs shape
Log-concavity with the explicit quadratic prefactor on the pair space
The identity function is log-concave on the positive ray

ASTIS mathematical exposition

Positive log-concavity on a domain

AutoSamplingTheory.TechnicalLemmas.Geometry.LogConcavity.LogConcaveOn · def · Teaching coverage

Statement

Let E be a real module, s⊆E any set, and f:E→ℝ. Define positive log-concavity on s to mean that f is strictly positive at every point of s and log f is concave on s. Concavity includes convexity of s. This definition imposes no condition on f outside s.

\[\operatorname{LC}_s(f)\ :\Longleftrightarrow\ \bigl[\forall x\in s,\ f(x)>0\bigr]\ \land\ \bigl[s\text{ convex and }\forall x,y\in s,\ a,b\ge0,\ a+b=1:\ a\log f(x)+b\log f(y)\le\log f(ax+by)\bigr].\]

All objects and hypotheses

E : Type* with [AddCommMonoid E] and [Module ℝ E]. These are the exact algebraic ambient structures; no topology, norm, measure or finite-dimensionality is assumed.
s : Set E and f : E → ℝ are arbitrary; positivity and concavity are clauses of the definition, not input hypotheses.

{'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.'}

Construction and meaning

1. Require genuine positivity on the domain

The first clause ensures that each logarithm refers to the usual logarithm of a positive real value. This excludes functions that vanish inside s; it does not rely on Lean's totalized value of log at zero or a negative number.

\[\forall x\in s,\quad 0<f(x).\]

Corresponding Lean step

(∀ x ∈ s, 0 < f x)

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

2. Require a convex domain and the concavity inequality

The second clause invokes Mathlib's ConcaveOn predicate for x↦log f(x). Its first component says s is convex, and its second is the displayed weighted inequality. Joining both clauses defines the predicate; there is no theorem proof here.

\[x,y\in s,\quad a,b\ge0,\quad a+b=1\ \Longrightarrow\ ax+by\in s,\quad a\log f(x)+b\log f(y)\le\log f(ax+by).\]

Corresponding Lean step

∧ ConcaveOn ℝ s (fun x => Real.log (f x))

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

Braces name inputs Lean can infer, and bracketed classes state the ambient structures listed above. This declaration defines a proposition; its two clauses specify what the property means. The result type Prop means this defines a property, not a new function or probability measure. The two sides of ∧ are positivity and concavity of the logarithm.

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.

def LogConcaveOn {E : Type*} [AddCommMonoid E] [Module ℝ E]
    (s : Set E) (f : E → ℝ) : Prop

Exact module and namespace context

Lean construction · LogConcaveOn

The result type Prop means this defines a property, not a new function or probability measure. The two sides of ∧ are positivity and concavity of the logarithm.

def LogConcaveOn {E : Type*} [AddCommMonoid E] [Module ℝ E]
    (s : Set E) (f : E → ℝ) : Prop :=
  (∀ x ∈ s, 0 < f x) ∧ ConcaveOn ℝ s (fun x => Real.log (f x))

Exact module and namespace context

Scope and omitted-condition boundaries

This convention is stricter than a nonnegative extended-log definition allowing zeros on the domain. No equivalence with that broader convention is asserted.
The domain may be empty; convexity and pointwise requirements then hold vacuously.
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)

ConcaveOn
Real.log

Mathematical sources

Existing ASTIS declaration and exact proof — Directly read current local source; no Lean edit or fresh build.
Existing curated module card — Local API/source-boundary memory; not independent primary textbook verification.
ConcaveOn — Exact inspected Mathlib definition or theorem used by this exposition.
Existing usage in Tests.Basic — Read-only source example; no test was run.
Existing usage in Tests.Basic — Read-only source example; no test was run.
Real.log — Exact local Mathlib declaration anchor.

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

ASTIS mathematical exposition

Unpack the definition of positive log-concavity

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

Statement

For any real module E, set s⊆E and function f:E→ℝ, positive log-concavity on s is equivalent to strict positivity of f on s together with concavity of its logarithm on s.

\[\operatorname{LC}_s(f)\iff(\forall x\in s,\ 0<f(x))\land\operatorname{Concave}_s(\log f).\]

All objects and hypotheses

E : Type* with [AddCommMonoid E] and [Module ℝ E]. These are the exact algebraic ambient structures; no topology, norm, measure or finite-dimensionality is assumed.
s : Set E; f : E → ℝ; no additional hypothesis.

{'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. Expand the named predicate

The left side was defined to be exactly the conjunction on the right. Therefore both directions are the identity implication; no analytical argument or new log-concavity criterion is added.

\[\operatorname{LC}_s(f)=(\text{positivity on }s)\land(\text{concavity of }\log f\text{ on }s).\]

Corresponding Lean step

Iff.rfl

Iff.rfl is reflexivity of an equivalence after expanding a definition.

Lean statement · logConcaveOn_iff

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. ↔ asks for equivalence in both directions. Iff.rfl proves it because expanding the definition gives literally the same proposition.

theorem logConcaveOn_iff {E : Type*} [AddCommMonoid E] [Module ℝ E]
    {s : Set E} {f : E → ℝ} :
    LogConcaveOn s f ↔
      (∀ x ∈ s, 0 < f x) ∧ ConcaveOn ℝ s (fun x => Real.log (f x))

Exact module and namespace context

Lean proof · logConcaveOn_iff

↔ asks for equivalence in both directions. Iff.rfl proves it because expanding the definition gives literally the same proposition.

theorem logConcaveOn_iff {E : Type*} [AddCommMonoid E] [Module ℝ E]
    {s : Set E} {f : E → ℝ} :
    LogConcaveOn s f ↔
      (∀ x ∈ s, 0 < f x) ∧ ConcaveOn ℝ s (fun x => Real.log (f x)) :=
  Iff.rfl

Exact module and namespace context

Scope and omitted-condition boundaries

Definition-level interface only; not a new mathematical characterization by geometric means or densities.
This documentation adds no Lean theorem, compilation evidence, source-equivalence verdict, or new source-fidelity certification.

Source and reuse

ASTIS parents called

AutoSamplingTheory.TechnicalLemmas.Geometry.LogConcavity.LogConcaveOn

Mathlib API called (external library)

No direct Mathlib call recorded; see the ASTIS parents.

Mathematical sources

Existing ASTIS declaration and exact proof — Directly read current local source; no Lean edit or fresh build.
Existing curated module card — Local API/source-boundary memory; not independent primary textbook verification.

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

ASTIS mathematical exposition

Build a log-concavity proof from its two ingredients

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

Statement

Let E be a real module, s⊆E, and f:E→ℝ. If f(x)>0 for every x∈s and log f is concave on s, then f is positive log-concave on s.

\[\bigl[\forall x\in s,\ 0<f(x)\bigr]\land\operatorname{Concave}_s(\log f)\Longrightarrow\operatorname{LC}_s(f).\]

All objects and hypotheses

E : Type* with [AddCommMonoid E] and [Module ℝ E]. These are the exact algebraic ambient structures; no topology, norm, measure or finite-dimensionality is assumed.
s : Set E and f : E → ℝ.
hpos : ∀ x∈s, 0<f x.
hlog : ConcaveOn ℝ s (fun x => Real.log (f x)); this already includes convexity of s.

{'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. Package positivity and log-concavity

The target predicate consists of precisely the two supplied facts. Put hpos in its first component and hlog in its second.

\[\bigl[(\forall x\in s,\ f(x)>0)\ \land\ \operatorname{ConcaveOn}(s,\log f)\bigr]\ \Longrightarrow\ \operatorname{LC}_s(f).\]

Corresponding Lean step

⟨hpos, hlog⟩

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_of_concave_log

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. The angle brackets construct a proof of a conjunction from its two proofs. Neither positivity nor concavity is derived here; both are explicit inputs.

theorem logConcaveOn_of_concave_log {E : Type*} [AddCommMonoid E] [Module ℝ E]
    {s : Set E} {f : E → ℝ}
    (hpos : ∀ x ∈ s, 0 < f x)
    (hlog : ConcaveOn ℝ s (fun x => Real.log (f x))) :
    LogConcaveOn s f

Exact module and namespace context

Lean proof · logConcaveOn_of_concave_log

The angle brackets construct a proof of a conjunction from its two proofs. Neither positivity nor concavity is derived here; both are explicit inputs.

theorem logConcaveOn_of_concave_log {E : Type*} [AddCommMonoid E] [Module ℝ E]
    {s : Set E} {f : E → ℝ}
    (hpos : ∀ x ∈ s, 0 < f x)
    (hlog : ConcaveOn ℝ s (fun x => Real.log (f x))) :
    LogConcaveOn s f :=
  ⟨hpos, hlog⟩

Exact module and namespace context

Scope and omitted-condition boundaries

Constructor/reuse interface only.
This documentation adds no Lean theorem, compilation evidence, source-equivalence verdict, or new source-fidelity certification.

Source and reuse

ASTIS parents called

AutoSamplingTheory.TechnicalLemmas.Geometry.LogConcavity.LogConcaveOn

Mathlib API called (external library)

ConcaveOn

Mathematical sources

Existing ASTIS declaration and exact proof — Directly read current local source; no Lean edit or fresh build.
Existing curated module card — Local API/source-boundary memory; not independent primary textbook verification.
ConcaveOn — Exact inspected Mathlib definition or theorem used by this exposition.

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

ASTIS mathematical exposition

A positive log-concave function is positive at each domain point

AutoSamplingTheory.TechnicalLemmas.Geometry.LogConcavity.LogConcaveOn.pos · theorem · Teaching coverage

Statement

Let E be a real module, f:E→ℝ positive log-concave on s⊆E, and x∈s. Then f(x)>0.

\[\operatorname{LC}_s(f),\quad x\in s\quad\Longrightarrow\quad f(x)>0.\]

All objects and hypotheses

E : Type* with [AddCommMonoid E] and [Module ℝ E]. These are the exact algebraic ambient structures; no topology, norm, measure or finite-dimensionality is assumed.
s : Set E, f : E → ℝ, hf : LogConcaveOn s f.
x : E with hx : x∈s.

{'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 the positivity component at x

Positive log-concavity includes a proof that f is positive at every domain point. Apply that proof to the particular x and its membership hypothesis.

\[(\forall z\in s,\ 0<f(z))\Longrightarrow 0<f(x).\]

Corresponding Lean step

hf.1 x hx

The .1 field is the positivity component; the following arguments specify the point and its membership.

Lean statement · pos

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. hf.1 selects the first component of the conjunction; x hx supplies the point and its membership proof.

theorem LogConcaveOn.pos {E : Type*} [AddCommMonoid E] [Module ℝ E]
    {s : Set E} {f : E → ℝ}
    (hf : LogConcaveOn s f) {x : E} (hx : x ∈ s) :
    0 < f x

Exact module and namespace context

Lean proof · pos

hf.1 selects the first component of the conjunction; x hx supplies the point and its membership proof.

theorem LogConcaveOn.pos {E : Type*} [AddCommMonoid E] [Module ℝ E]
    {s : Set E} {f : E → ℝ}
    (hf : LogConcaveOn s f) {x : E} (hx : x ∈ s) :
    0 < f x :=
  hf.1 x hx

Exact module and namespace context

Scope and omitted-condition boundaries

No assertion about f outside s; positivity is extracted from the chosen definition, not deduced from concavity of log alone.
This documentation adds no Lean theorem, compilation evidence, source-equivalence verdict, or new source-fidelity certification.

Source and reuse

ASTIS parents called

AutoSamplingTheory.TechnicalLemmas.Geometry.LogConcavity.LogConcaveOn

Mathlib API called (external library)

No direct Mathlib call recorded; see the ASTIS parents.

Mathematical sources

Existing ASTIS declaration and exact proof — Directly read current local source; no Lean edit or fresh build.
Existing curated module card — Local API/source-boundary memory; not independent primary textbook verification.

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

ASTIS mathematical exposition

Read the concavity of the logarithm

AutoSamplingTheory.TechnicalLemmas.Geometry.LogConcavity.LogConcaveOn.concaveOn_log · theorem · Teaching coverage

Statement

Let E be a real module and f:E→ℝ positive log-concave on s⊆E. Then x↦log f(x) is concave on s, including convexity of the domain.

\[\operatorname{LC}_s(f)\Longrightarrow\operatorname{Concave}_s(\log f).\]

All objects and hypotheses

E : Type* with [AddCommMonoid E] and [Module ℝ E]. These are the exact algebraic ambient structures; no topology, norm, measure or finite-dimensionality is assumed.
s : Set E, f : E → ℝ, hf : LogConcaveOn s f.

{'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. Extract the second defining clause

The second component of positive log-concavity is already the requested concavity statement. Return it unchanged.

\[a\log f(x)+b\log f(y)\le\log f(ax+by)\quad(x,y\in s,\ a,b\ge0,\ a+b=1).\]

Corresponding Lean step

hf.2

The .2 field is the concavity component already stored in the supplied hypothesis.

Lean statement · concaveOn_log

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. hf.2 projects the second half of the definition. ConcaveOn itself records both the domain and its Jensen inequality.

theorem LogConcaveOn.concaveOn_log {E : Type*} [AddCommMonoid E] [Module ℝ E]
    {s : Set E} {f : E → ℝ}
    (hf : LogConcaveOn s f) :
    ConcaveOn ℝ s (fun x => Real.log (f x))

Exact module and namespace context

Lean proof · concaveOn_log

hf.2 projects the second half of the definition. ConcaveOn itself records both the domain and its Jensen inequality.

theorem LogConcaveOn.concaveOn_log {E : Type*} [AddCommMonoid E] [Module ℝ E]
    {s : Set E} {f : E → ℝ}
    (hf : LogConcaveOn s f) :
    ConcaveOn ℝ s (fun x => Real.log (f x)) :=
  hf.2

/-- The negative logarithm of a positive log-concave function is convex. -/

Exact module and namespace context

Scope and omitted-condition boundaries

Projection only; no new concavity theorem is proved.
This documentation adds no Lean theorem, compilation evidence, source-equivalence verdict, or new source-fidelity certification.

Source and reuse

ASTIS parents called

AutoSamplingTheory.TechnicalLemmas.Geometry.LogConcavity.LogConcaveOn

Mathlib API called (external library)

ConcaveOn

Mathematical sources

Existing ASTIS declaration and exact proof — Directly read current local source; no Lean edit or fresh build.
Existing curated module card — Local API/source-boundary memory; not independent primary textbook verification.
ConcaveOn — Exact inspected Mathlib definition or theorem used by this exposition.

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

ASTIS mathematical exposition

The negative logarithm is a convex potential

AutoSamplingTheory.TechnicalLemmas.Geometry.LogConcavity.LogConcaveOn.convexOn_neg_log · theorem · Teaching coverage

Statement

Let E be a real module and f:E→ℝ positive log-concave on s⊆E. Then V(x)=−log f(x) is convex on s.

\[\operatorname{LC}_s(f)\Longrightarrow \operatorname{Convex}_s(V),\qquad V=-\log f,\quad V(ax+by)\le aV(x)+bV(y).\]

All objects and hypotheses

E : Type* with [AddCommMonoid E] and [Module ℝ E]. These are the exact algebraic ambient structures; no topology, norm, measure or finite-dimensionality is assumed.
s : Set E, f : E → ℝ, hf : LogConcaveOn s f.

{'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 the concavity inequality

Positive log-concavity supplies convexity of s and the lower bound on log f at a convex combination.

\[a\log f(x)+b\log f(y)\le\log f(ax+by).\]

Corresponding Lean step

hf.concaveOn_log

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

2. Negate the inequality

Multiplication by −1 reverses the inequality, giving the convexity inequality for −log f on the same convex domain. Mathlib packages this exact sign reversal.

\[-\log f(ax+by)\le a[-\log f(x)]+b[-\log f(y)].\]

Corresponding Lean step

change ConvexOn ℝ s (-(fun x => Real.log (f x)))
exact hf.concaveOn_log.neg

Negation reverses the inequality and exchanges convexity with concavity.

Lean statement · convexOn_neg_log

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. The minus sign outside a function is pointwise negation. The .neg theorem changes concavity into convexity by reversing its inequality.

theorem LogConcaveOn.convexOn_neg_log {E : Type*} [AddCommMonoid E] [Module ℝ E]
    {s : Set E} {f : E → ℝ}
    (hf : LogConcaveOn s f) :
    ConvexOn ℝ s (fun x => - Real.log (f x))

Exact module and namespace context

Lean proof · convexOn_neg_log

The minus sign outside a function is pointwise negation. The .neg theorem changes concavity into convexity by reversing its inequality.

theorem LogConcaveOn.convexOn_neg_log {E : Type*} [AddCommMonoid E] [Module ℝ E]
    {s : Set E} {f : E → ℝ}
    (hf : LogConcaveOn s f) :
    ConvexOn ℝ s (fun x => - Real.log (f x)) := by
  change ConvexOn ℝ s (-(fun x => Real.log (f x)))
  exact hf.concaveOn_log.neg

/-- Sublevel sets of the negative-log potential of a positive log-concave
function are convex. -/

Exact module and namespace context

Scope and omitted-condition boundaries

Potential convexity only; no differentiability, strong convexity, normalizing integral or measure is supplied.
This documentation adds no Lean theorem, compilation evidence, source-equivalence verdict, or new source-fidelity certification.

Source and reuse

ASTIS parents called

AutoSamplingTheory.TechnicalLemmas.Geometry.LogConcavity.LogConcaveOn.concaveOn_log

Mathlib API called (external library)

ConcaveOn.neg

Mathematical sources

Existing ASTIS declaration and exact proof — Directly read current local source; no Lean edit or fresh build.
Existing curated module card — Local API/source-boundary memory; not independent primary textbook verification.
ConcaveOn.neg — Exact inspected Mathlib definition or theorem used by this exposition.
Existing usage in Tests.Basic — Read-only source example; no test was run.

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

ASTIS mathematical exposition

Sublevel sets of the negative-log potential are convex

AutoSamplingTheory.TechnicalLemmas.Geometry.LogConcavity.LogConcaveOn.convex_sublevel_neg_log · theorem · Teaching coverage

Statement

Let E be a real module, f:E→ℝ positive log-concave on s⊆E, and r∈ℝ any threshold. The set of x∈s with −log f(x)≤r is convex.

\[\operatorname{LC}_s(f)\Longrightarrow\{x\in s:-\log f(x)\le r\}\text{ is convex}\quad(r\in\mathbb R).\]

All objects and hypotheses

E : Type* with [AddCommMonoid E] and [Module ℝ E]. These are the exact algebraic ambient structures; no topology, norm, measure or finite-dimensionality is assumed.
s : Set E, f : E → ℝ, hf : LogConcaveOn s f.
r : ℝ is arbitrary, with no sign restriction.

{'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. Use the convex negative-log potential

The preceding result gives a convex function V=−log f on s.

\[V(ax+by)\le aV(x)+bV(y).\]

Corresponding Lean step

hf.convexOn_neg_log

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

2. Bound a convex combination of two sublevel points

If V(x),V(y)≤r and a,b≥0 sum to one, then their weighted potential bound is at most ar+br=r. Convexity of s keeps the combination in s. This is precisely the sublevel-set theorem bundled as quasiconvexity.

\[V(ax+by)\le aV(x)+bV(y)\le ar+br=r.\]

Corresponding Lean step

hf.convexOn_neg_log.quasiconvexOn r

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 · convex_sublevel_neg_log

theorem LogConcaveOn.convex_sublevel_neg_log {E : Type*} [AddCommMonoid E] [Module ℝ E]
    {s : Set E} {f : E → ℝ}
    (hf : LogConcaveOn s f) (r : ℝ) :
    Convex ℝ {x ∈ s | - Real.log (f x) ≤ r}

Exact module and namespace context

Lean proof · convex_sublevel_neg_log

quasiconvexOn says every sublevel set is convex. Applying it to r selects the desired set.

theorem LogConcaveOn.convex_sublevel_neg_log {E : Type*} [AddCommMonoid E] [Module ℝ E]
    {s : Set E} {f : E → ℝ}
    (hf : LogConcaveOn s f) (r : ℝ) :
    Convex ℝ {x ∈ s | - Real.log (f x) ≤ r} :=
  hf.convexOn_neg_log.quasiconvexOn r

Exact module and namespace context

Scope and omitted-condition boundaries

The set is restricted to s; no claim about sublevels outside the given domain.
This documentation adds no Lean theorem, compilation evidence, source-equivalence verdict, or new source-fidelity certification.

Source and reuse

ASTIS parents called

AutoSamplingTheory.TechnicalLemmas.Geometry.LogConcavity.LogConcaveOn.convexOn_neg_log

Mathlib API called (external library)

ConvexOn.quasiconvexOn

Mathematical sources

Existing ASTIS declaration and exact proof — Directly read current local source; no Lean edit or fresh build.
Existing curated module card — Local API/source-boundary memory; not independent primary textbook verification.
ConvexOn.quasiconvexOn — Exact inspected Mathlib definition or theorem used by this exposition.
Existing usage in Tests.Basic — Read-only source example; no test was run.

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

ASTIS mathematical exposition

The log-concavity domain is convex

AutoSamplingTheory.TechnicalLemmas.Geometry.LogConcavity.LogConcaveOn.convex_domain · theorem · Teaching coverage

Statement

Let E be a real module and f:E→ℝ positive log-concave on s⊆E. Then s is convex.

\[\operatorname{LC}_s(f)\Longrightarrow\forall x,y\in s,\ a,b\ge0,\ a+b=1:\ ax+by\in s.\]

All objects and hypotheses

E : Type* with [AddCommMonoid E] and [Module ℝ E]. These are the exact algebraic ambient structures; no topology, norm, measure or finite-dimensionality is assumed.
s : Set E, f : E → ℝ, hf : LogConcaveOn s f.

{'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 the domain clause of log concavity

ConcaveOn(log f) contains convexity of s as its first field. Extract that field; it was required by the definition and is not newly inferred from a pointwise inequality on a nonconvex domain.

\[\operatorname{Concave}_s(\log f)=\bigl[s\text{ convex}\bigr]\land[\text{concavity inequality}].\]

Corresponding Lean step

hf.concaveOn_log.1

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 · convex_domain

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. The first .1 extracts the convex-domain component from ConcaveOn. The theorem is a convenient interface to stored information.

theorem LogConcaveOn.convex_domain {E : Type*} [AddCommMonoid E] [Module ℝ E]
    {s : Set E} {f : E → ℝ}
    (hf : LogConcaveOn s f) :
    Convex ℝ s

Exact module and namespace context

Lean proof · convex_domain

The first .1 extracts the convex-domain component from ConcaveOn. The theorem is a convenient interface to stored information.

theorem LogConcaveOn.convex_domain {E : Type*} [AddCommMonoid E] [Module ℝ E]
    {s : Set E} {f : E → ℝ}
    (hf : LogConcaveOn s f) :
    Convex ℝ s :=
  hf.concaveOn_log.1

/-- Superlevel sets of a positive log-concave function are convex within the
log-concavity domain. -/

Exact module and namespace context

Scope and omitted-condition boundaries

Do not describe this as proving convexity for an arbitrary support of a nonnegative density.
This documentation adds no Lean theorem, compilation evidence, source-equivalence verdict, or new source-fidelity certification.

Source and reuse

ASTIS parents called

AutoSamplingTheory.TechnicalLemmas.Geometry.LogConcavity.LogConcaveOn.concaveOn_log

Mathlib API called (external library)

ConcaveOn

Mathematical sources

Existing ASTIS declaration and exact proof — Directly read current local source; no Lean edit or fresh build.
Existing curated module card — Local API/source-boundary memory; not independent primary textbook verification.
ConcaveOn — Exact inspected Mathlib definition or theorem used by this exposition.

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

ASTIS mathematical exposition

Every superlevel set of a positive log-concave function is convex

AutoSamplingTheory.TechnicalLemmas.Geometry.LogConcavity.LogConcaveOn.convex_superlevel · theorem · Teaching coverage

Statement

Let E be a real module, f:E→ℝ positive log-concave on s⊆E, and c∈ℝ. Then S_c={x∈s:c≤f(x)} is convex. No positivity assumption on c is needed.

\[S_c=\{x\in s:f(x)\ge c\},\qquad \operatorname{LC}_s(f)\Longrightarrow S_c\text{ convex for every }c\in\mathbb R.\]

All objects and hypotheses

E : Type* with [AddCommMonoid E] and [Module ℝ E]. These are the exact algebraic ambient structures; no topology, norm, measure or finite-dimensionality is assumed.
s : Set E, f : E → ℝ, hf : LogConcaveOn s f.
c : ℝ arbitrary. In the proof x,y∈S_c and a,b≥0 with a+b=1; set z=ax+by.

{'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. Handle nonpositive thresholds directly

If c≤0, every point of s belongs to S_c because f is strictly positive there. For x,y∈S_c, convexity of s puts z in s and hence f(z)>0≥c. This proves the case c≤0 without taking log c.

\[c\le0\Longrightarrow S_c=s,\qquad f(z)>0\ge c.\]

Corresponding Lean step

by_cases hc : c ≤ 0
· intro x hx y hy a b ha hb hab
  have hmid_s := hf.convex_domain hx.1 hy.1 ha hb hab
  exact ⟨hmid_s, le_of_lt (lt_of_le_of_lt hc (hf.pos (x := a • x + b • y) hmid_s))⟩

hmid records domain membership of the convex combination, permitting the same positivity assumptions at that point.

2. For c>0, compare endpoint logarithms

In the remaining case c is positive. Both endpoints satisfy c≤f(x),f(y), so monotonicity of log gives log c≤log f(x),log f(y). The midpoint z lies in s by domain convexity and f(z)>0.

\[\log c\le\log f(x),\quad\log c\le\log f(y),\quad z\in s,\quad f(z)>0.\]

Corresponding Lean step

have hcpos : 0 < c := lt_of_not_ge hc
have hmid_s := hf.convex_domain hx.1 hy.1 ha hb hab
have hlogx := Real.log_le_log hcpos hx.2
have hlogy := Real.log_le_log hcpos hy.2

hmid records domain membership of the convex combination, permitting the same positivity assumptions at that point.

3. Form the weighted lower bound

Multiply the two endpoint inequalities by the nonnegative weights and add. Since a+b=1, the weighted sum of the two copies of log c is log c itself.

\[\log c=(a+b)\log c\le a\log f(x)+b\log f(y).\]

Corresponding Lean step

have hweighted := add_le_add (mul_le_mul_of_nonneg_left hlogx ha) (mul_le_mul_of_nonneg_left hlogy hb)
-- hconst uses a+b=1; hfloor rewrites this weighted bound.

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

4. Apply log concavity

The defining concavity inequality bounds the weighted endpoint logarithms by log f(z). Combining the bounds yields log c≤log f(z).

\[\log c\le a\log f(x)+b\log f(y)\le\log f(z).\]

Corresponding Lean step

have hconc : a * Real.log (f x) + b * Real.log (f y) ≤ Real.log (f (a • x + b • y)) := by
  simpa [smul_eq_mul] using hf.concaveOn_log.2 hx.1 hy.1 ha hb hab

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

5. Return from logarithms to the function values

Both c and f(z) are positive, so log is order-reflecting on these values. Thus c≤f(z); together with z∈s, this shows z∈S_c and proves convexity.

\[\log c\le\log f(z)\iff c\le f(z),\qquad z\in S_c.\]

Corresponding Lean step

exact (Real.log_le_log_iff hcpos (hf.pos (x := a • x + b • y) hmid_s)).mp (hfloor.trans hconc)

The two positivity proofs allow logarithms to reflect order; .mp selects the required implication.

Lean statement · convex_superlevel

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. The proof splits on c≤0 to avoid using logarithms outside their positive domain. Membership hx contains two facts: hx.1 is x∈s, and hx.2 is c≤f x. The final .mp takes the forward implication of the log-order equivalence.

theorem LogConcaveOn.convex_superlevel {E : Type*} [AddCommMonoid E] [Module ℝ E]
    {s : Set E} {f : E → ℝ}
    (hf : LogConcaveOn s f) (c : ℝ) :
    Convex ℝ {x ∈ s | c ≤ f x}

Exact module and namespace context

Lean proof · convex_superlevel

The proof splits on c≤0 to avoid using logarithms outside their positive domain. Membership hx contains two facts: hx.1 is x∈s, and hx.2 is c≤f x. The final .mp takes the forward implication of the log-order equivalence.

theorem LogConcaveOn.convex_superlevel {E : Type*} [AddCommMonoid E] [Module ℝ E]
    {s : Set E} {f : E → ℝ}
    (hf : LogConcaveOn s f) (c : ℝ) :
    Convex ℝ {x ∈ s | c ≤ f x} := by
  by_cases hc : c ≤ 0
  · intro x hx y hy a b ha hb hab
    have hmid_s := hf.convex_domain hx.1 hy.1 ha hb hab
    exact ⟨hmid_s, le_of_lt (lt_of_le_of_lt hc (hf.pos (x := a • x + b • y) hmid_s))⟩
  · have hcpos : 0 < c := lt_of_not_ge hc
    intro x hx y hy a b ha hb hab
    have hmid_s := hf.convex_domain hx.1 hy.1 ha hb hab
    refine ⟨hmid_s, ?_⟩
    have hlogx : Real.log c ≤ Real.log (f x) :=
      Real.log_le_log hcpos hx.2
    have hlogy : Real.log c ≤ Real.log (f y) :=
      Real.log_le_log hcpos hy.2
    have hweighted :
        a * Real.log c + b * Real.log c ≤
          a * Real.log (f x) + b * Real.log (f y) :=
      add_le_add (mul_le_mul_of_nonneg_left hlogx ha) (mul_le_mul_of_nonneg_left hlogy hb)
    have hconst : a * Real.log c + b * Real.log c = Real.log c := by
      calc
        a * Real.log c + b * Real.log c = (a + b) * Real.log c := by ring
        _ = Real.log c := by rw [hab]; ring
    have hfloor : Real.log c ≤ a * Real.log (f x) + b * Real.log (f y) := by
      simpa [hconst] using hweighted
    have hconc :
        a * Real.log (f x) + b * Real.log (f y) ≤
          Real.log (f (a • x + b • y)) := by
      simpa [smul_eq_mul] using hf.concaveOn_log.2 hx.1 hy.1 ha hb hab
    exact (Real.log_le_log_iff hcpos (hf.pos (x := a • x + b • y) hmid_s)).mp
      (hfloor.trans hconc)

/-- Positive log-concave functions are quasiconcave: all superlevel sets are convex. -/

Exact module and namespace context

Scope and omitted-condition boundaries

This is non-strict convexity of domain-restricted superlevels; no strict concavity, boundedness or compactness is asserted.
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.log_le_log
Real.log_le_log_iff
add_le_add
mul_le_mul_of_nonneg_left
lt_of_not_ge
le_of_lt
lt_of_le_of_lt
smul_eq_mul

Mathematical sources

Existing ASTIS declaration and exact proof — Directly read current local source; no Lean edit or fresh build.
Existing curated module card — Local API/source-boundary memory; not independent primary textbook verification.
Real.log_le_log — Exact inspected Mathlib definition or theorem used by this exposition.
Real.log_le_log_iff — Exact inspected Mathlib definition or theorem used by this exposition.
Existing usage in Tests.Basic — Read-only source example; no test was run.

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

ASTIS mathematical exposition

Positive log-concavity implies quasiconcavity

AutoSamplingTheory.TechnicalLemmas.Geometry.LogConcavity.LogConcaveOn.quasiconcaveOn · theorem · Teaching coverage

Statement

Let E be a real module and f:E→ℝ positive log-concave on s⊆E. Then f is quasiconcave on s: every superlevel set {x∈s:c≤f(x)}, for every real c, is convex.

\[\operatorname{LC}_s(f)\Longrightarrow\operatorname{Quasiconcave}_s(f)\equiv\forall c\in\mathbb R,\ \{x\in s:c\le f(x)\}\text{ convex}.\]

All objects and hypotheses

E : Type* with [AddCommMonoid E] and [Module ℝ E]. These are the exact algebraic ambient structures; no topology, norm, measure or finite-dimensionality is assumed.
s : Set E, f : E → ℝ, hf : LogConcaveOn s f.

{'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. Provide every superlevel-set instance

For an arbitrary threshold c, the already-proved convex_superlevel theorem gives exactly the convex set required by the definition of QuasiconcaveOn. Returning this family of proofs completes the assertion.

\[c\longmapsto[\{x\in s:c\le f(x)\}\text{ is convex}].\]

Corresponding Lean step

fun c => hf.convex_superlevel c

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 · quasiconcaveOn

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. fun c constructs a proof for every threshold. This declaration packages the preceding theorem in Mathlib's standard quasiconcavity predicate.

theorem LogConcaveOn.quasiconcaveOn {E : Type*} [AddCommMonoid E] [Module ℝ E]
    {s : Set E} {f : E → ℝ}
    (hf : LogConcaveOn s f) :
    QuasiconcaveOn ℝ s f

Exact module and namespace context

Lean proof · quasiconcaveOn

fun c constructs a proof for every threshold. This declaration packages the preceding theorem in Mathlib's standard quasiconcavity predicate.

theorem LogConcaveOn.quasiconcaveOn {E : Type*} [AddCommMonoid E] [Module ℝ E]
    {s : Set E} {f : E → ℝ}
    (hf : LogConcaveOn s f) :
    QuasiconcaveOn ℝ s f :=
  fun c => hf.convex_superlevel c

Exact module and namespace context

Scope and omitted-condition boundaries

Reuse wrapper around convex_superlevel, not an independent superlevel proof.
This documentation adds no Lean theorem, compilation evidence, source-equivalence verdict, or new source-fidelity certification.

Source and reuse

ASTIS parents called

AutoSamplingTheory.TechnicalLemmas.Geometry.LogConcavity.LogConcaveOn.convex_superlevel

Mathlib API called (external library)

QuasiconcaveOn

Mathematical sources

Existing ASTIS declaration and exact proof — Directly read current local source; no Lean edit or fresh build.
Existing curated module card — Local API/source-boundary memory; not independent primary textbook verification.
QuasiconcaveOn — Exact inspected Mathlib definition or theorem used by this exposition.
Existing usage in Tests.Basic — Read-only source example; no test was run.

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

ASTIS mathematical exposition

Restrict to a convex smaller domain

AutoSamplingTheory.TechnicalLemmas.Geometry.LogConcavity.LogConcaveOn.subset · theorem · Teaching coverage

Statement

Let E be a real module, f:E→ℝ positive log-concave on s⊆E, and t⊆s a convex set. Then the same function f is positive log-concave on t.

\[\operatorname{LC}_s(f),\quad t\subseteq s,\quad t\text{ convex}\Longrightarrow\operatorname{LC}_t(f).\]

All objects and hypotheses

E : Type* with [AddCommMonoid E] and [Module ℝ E]. These are the exact algebraic ambient structures; no topology, norm, measure or finite-dimensionality is assumed.
s,t : Set E; f : E → ℝ; hf : LogConcaveOn s f.
hts : t⊆s and ht : Convex ℝ t are both explicit assumptions.

{'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. Restrict positivity

Every x∈t lies in s, so the supplied positivity on s gives f(x)>0.

\[x\in t\subseteq s\Longrightarrow f(x)>0.\]

Corresponding Lean step

fun x hx => hf.pos (x := x) (hts 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. Restrict the concavity inequality on a convex domain

For x,y∈t, the original concavity inequality applies because both lie in s. Convexity of t supplies the required domain condition for the restricted predicate. Pair this concavity statement with positivity.

\[a\log f(x)+b\log f(y)\le\log f(ax+by),\qquad ax+by\in t.\]

Corresponding Lean step

⟨fun x hx => hf.pos (x := x) (hts hx), hf.concaveOn_log.subset hts ht⟩

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 · subset

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. Restricting a function's domain does not alter its values. The separate ht is necessary because LogConcaveOn includes convexity of the domain.

theorem LogConcaveOn.subset {E : Type*} [AddCommMonoid E] [Module ℝ E]
    {s t : Set E} {f : E → ℝ}
    (hf : LogConcaveOn s f) (hts : t ⊆ s) (ht : Convex ℝ t) :
    LogConcaveOn t f

Exact module and namespace context

Lean proof · subset

Restricting a function's domain does not alter its values. The separate ht is necessary because LogConcaveOn includes convexity of the domain.

theorem LogConcaveOn.subset {E : Type*} [AddCommMonoid E] [Module ℝ E]
    {s t : Set E} {f : E → ℝ}
    (hf : LogConcaveOn s f) (hts : t ⊆ s) (ht : Convex ℝ t) :
    LogConcaveOn t f :=
  ⟨fun x hx => hf.pos (x := x) (hts hx), hf.concaveOn_log.subset hts ht⟩

/-- Restricting a positive log-concave function to one of its superlevel sets
preserves log-concavity. -/

Exact module and namespace context

Scope and omitted-condition boundaries

Arbitrary nonconvex restrictions are not allowed by this predicate.
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)

ConcaveOn.subset

Mathematical sources

Existing ASTIS declaration and exact proof — Directly read current local source; no Lean edit or fresh build.
Existing curated module card — Local API/source-boundary memory; not independent primary textbook verification.
ConcaveOn.subset — Exact inspected Mathlib definition or theorem used by this exposition.

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

ASTIS mathematical exposition

Restrict log-concavity to a superlevel set

AutoSamplingTheory.TechnicalLemmas.Geometry.LogConcavity.LogConcaveOn.restrict_superlevel · theorem · Teaching coverage

Statement

Let E be a real module, f:E→ℝ positive log-concave on s⊆E, and c∈ℝ arbitrary. The function f remains positive log-concave on the domain {x∈s:c≤f(x)}.

\[\operatorname{LC}_s(f)\Longrightarrow\operatorname{LC}_{\{x\in s:c\le f(x)\}}(f).\]

All objects and hypotheses

E : Type* with [AddCommMonoid E] and [Module ℝ E]. These are the exact algebraic ambient structures; no topology, norm, measure or finite-dimensionality is assumed.
s : Set E, f : E → ℝ, hf : LogConcaveOn s f.
c : ℝ, with no sign restriction.

{'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. Check the restricted domain fits the restriction theorem

A superlevel point is in s by definition, and the superlevel set is convex by convex_superlevel. These are exactly the two requirements of LogConcaveOn.subset.

\[S_c=\{x\in s:c\le f(x)\}\subseteq s,\qquad S_c\text{ convex}.\]

Corresponding Lean step

(fun _ hx => hx.1)
(hf.convex_superlevel c)

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 convex-domain restriction

Apply the restriction theorem to those facts; it preserves the supplied positivity and logarithmic concavity on the smaller domain.

\[\operatorname{LC}_s(f)\Longrightarrow\operatorname{LC}_{S_c}(f).\]

Corresponding Lean step

hf.subset (fun _ hx => hx.1) (hf.convex_superlevel c)

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 · restrict_superlevel

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. hx.1 forgets the superlevel inequality and keeps only membership in s. The rest is a direct use of two previous results.

theorem LogConcaveOn.restrict_superlevel {E : Type*} [AddCommMonoid E] [Module ℝ E]
    {s : Set E} {f : E → ℝ}
    (hf : LogConcaveOn s f) (c : ℝ) :
    LogConcaveOn {x ∈ s | c ≤ f x} f

Exact module and namespace context

Lean proof · restrict_superlevel

hx.1 forgets the superlevel inequality and keeps only membership in s. The rest is a direct use of two previous results.

theorem LogConcaveOn.restrict_superlevel {E : Type*} [AddCommMonoid E] [Module ℝ E]
    {s : Set E} {f : E → ℝ}
    (hf : LogConcaveOn s f) (c : ℝ) :
    LogConcaveOn {x ∈ s | c ≤ f x} f :=
  hf.subset (fun _ hx => hx.1) (hf.convex_superlevel c)

/-- Precomposition by a linear map preserves log-concavity on the preimage domain. -/

Exact module and namespace context

Scope and omitted-condition boundaries

No new function is defined by setting f to zero outside the superlevel set; only its asserted domain is restricted.
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)

No direct Mathlib call recorded; see the ASTIS parents.

Mathematical sources

Existing ASTIS declaration and exact proof — Directly read current local source; no Lean edit or fresh build.
Existing curated module card — Local API/source-boundary memory; not independent primary textbook verification.
Existing usage in Tests.Basic — Read-only source example; no test was run.

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

ASTIS mathematical exposition

Log-concavity survives linear precomposition

AutoSamplingTheory.TechnicalLemmas.Geometry.LogConcavity.LogConcaveOn.comp_linearMap · theorem · Teaching coverage

Statement

Let E and F be real modules, s⊆F and f:F→ℝ positive log-concave on s. For any linear map g:E→F, the composite x↦f(g(x)) is positive log-concave on the inverse-image domain g⁻¹(s). The map need not be injective or surjective.

\[\operatorname{LC}_s(f)\Longrightarrow\operatorname{LC}_{g^{-1}(s)}(f\circ g).\]

All objects and hypotheses

E,F : Type* with [AddCommMonoid E] [Module ℝ E] [AddCommMonoid F] [Module ℝ F]. No topological or measure structures are assumed.
s : Set F, f : F → ℝ, hf : LogConcaveOn s f.
g : E →ₗ[ℝ] F is an ℝ-linear map.

{'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. Pull positivity back to the input space

If x belongs to g⁻¹(s), then g(x)∈s, so the original positivity gives f(g(x))>0.

\[x\in g^{-1}(s)\Longrightarrow g(x)\in s\Longrightarrow f(g(x))>0.\]

Corresponding Lean step

refine ⟨fun x hx => hf.pos (x := g x) hx, ?_⟩

The two components requested here are the exact clauses of the predicate, not extra hypotheses.

2. Use preservation of convex combinations

The map g preserves combinations ax+by with nonnegative coefficients summing to one. Consequently g⁻¹(s) is convex and the logarithmic concavity inequality on s transfers to the composite. Mathlib's precomposition theorem packages this calculation.

\[g(ax+by)=ag(x)+bg(y),\quad a\log f(g(x))+b\log f(g(y))\le\log f(g(ax+by)).\]

Corresponding Lean step

simpa [Function.comp_def] using hf.concaveOn_log.comp_linearMap g

The linear-map API pulls back the domain and applies the existing inequality to mapped endpoints.

Lean statement · comp_linearMap

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. The inverse-image domain ensures every argument sent to f lies where its assumptions hold. The final simplification writes composition as function application; it does not change the mathematical domain.

theorem LogConcaveOn.comp_linearMap {E F : Type*}
    [AddCommMonoid E] [Module ℝ E] [AddCommMonoid F] [Module ℝ F]
    {s : Set F} {f : F → ℝ}
    (hf : LogConcaveOn s f) (g : E →ₗ[ℝ] F) :
    LogConcaveOn (g ⁻¹' s) (fun x : E => f (g x))

Exact module and namespace context

Lean proof · comp_linearMap

The inverse-image domain ensures every argument sent to f lies where its assumptions hold. The final simplification writes composition as function application; it does not change the mathematical domain.

theorem LogConcaveOn.comp_linearMap {E F : Type*}
    [AddCommMonoid E] [Module ℝ E] [AddCommMonoid F] [Module ℝ F]
    {s : Set F} {f : F → ℝ}
    (hf : LogConcaveOn s f) (g : E →ₗ[ℝ] F) :
    LogConcaveOn (g ⁻¹' s) (fun x : E => f (g x)) := by
  refine ⟨fun x hx => hf.pos (x := g x) hx, ?_⟩
  simpa [Function.comp_def] using hf.concaveOn_log.comp_linearMap g

/-- Precomposition by an affine map preserves log-concavity on the preimage domain. -/

Exact module and namespace context

Scope and omitted-condition boundaries

Only precomposition, not integration/marginalization, is proved. No continuity, measurability, invertibility or determinant condition is used.
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)

ConcaveOn.comp_linearMap
Function.comp_def

Mathematical sources

Existing ASTIS declaration and exact proof — Directly read current local source; no Lean edit or fresh build.
Existing curated module card — Local API/source-boundary memory; not independent primary textbook verification.
ConcaveOn.comp_linearMap — Exact inspected Mathlib definition or theorem used by this exposition.
Existing usage in Tests.Basic — Read-only source example; no test was run.

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

ASTIS mathematical exposition

Log-concavity survives affine precomposition

AutoSamplingTheory.TechnicalLemmas.Geometry.LogConcavity.LogConcaveOn.comp_affineMap · theorem · Teaching coverage

Statement

Let E and F be real modules with additive commutative-group structures, s⊆F and f:F→ℝ positive log-concave on s. For any affine map g:E→F, the composite x↦f(g(x)) is positive log-concave on the inverse-image domain g⁻¹(s). The map need not be injective or surjective.

\[\operatorname{LC}_s(f)\Longrightarrow\operatorname{LC}_{g^{-1}(s)}(f\circ g).\]

All objects and hypotheses

E,F : Type* with [AddCommGroup E] [Module ℝ E] [AddCommGroup F] [Module ℝ F], exactly as required by the affine-map theorem. No topological or measure structures are assumed.
s : Set F, f : F → ℝ, hf : LogConcaveOn s f.
g : E →ᵃ[ℝ] F is an affine map.

{'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. Pull positivity back to the input space

If x belongs to g⁻¹(s), then g(x)∈s, so the original positivity gives f(g(x))>0.

\[x\in g^{-1}(s)\Longrightarrow g(x)\in s\Longrightarrow f(g(x))>0.\]

Corresponding Lean step

refine ⟨fun x hx => hf.pos (x := g x) hx, ?_⟩

The two components requested here are the exact clauses of the predicate, not extra hypotheses.

2. Use preservation of convex combinations

\[g(ax+by)=ag(x)+bg(y),\quad a\log f(g(x))+b\log f(g(y))\le\log f(g(ax+by)).\]

Corresponding Lean step

simpa [Function.comp_def] using hf.concaveOn_log.comp_affineMap g

The affine-map API uses preservation of convex combinations, including that the coefficients sum to one.

Lean statement · comp_affineMap

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. The inverse-image domain ensures every argument sent to f lies where its assumptions hold. The final simplification writes composition as function application; it does not change the mathematical domain.

theorem LogConcaveOn.comp_affineMap {E F : Type*}
    [AddCommGroup E] [Module ℝ E] [AddCommGroup F] [Module ℝ F]
    {s : Set F} {f : F → ℝ}
    (hf : LogConcaveOn s f) (g : E →ᵃ[ℝ] F) :
    LogConcaveOn (g ⁻¹' s) (fun x : E => f (g x))

Exact module and namespace context

Lean proof · comp_affineMap

theorem LogConcaveOn.comp_affineMap {E F : Type*}
    [AddCommGroup E] [Module ℝ E] [AddCommGroup F] [Module ℝ F]
    {s : Set F} {f : F → ℝ}
    (hf : LogConcaveOn s f) (g : E →ᵃ[ℝ] F) :
    LogConcaveOn (g ⁻¹' s) (fun x : E => f (g x)) := by
  refine ⟨fun x hx => hf.pos (x := g x) hx, ?_⟩
  simpa [Function.comp_def] using hf.concaveOn_log.comp_affineMap g

/-- The pointwise product of two positive log-concave functions on the same
domain is log-concave. -/

Exact module and namespace context

Scope and omitted-condition boundaries

Only precomposition, not integration/marginalization, is proved. No continuity, measurability, invertibility or determinant condition is used.
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)

ConcaveOn.comp_affineMap
Function.comp_def

Mathematical sources

Existing ASTIS declaration and exact proof — Directly read current local source; no Lean edit or fresh build.
Existing curated module card — Local API/source-boundary memory; not independent primary textbook verification.
ConcaveOn.comp_affineMap — Exact inspected Mathlib definition or theorem used by this exposition.
Existing usage in Tests.Basic — Read-only source example; no test was run.

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

ASTIS mathematical exposition

Products on a common domain preserve positive log-concavity

AutoSamplingTheory.TechnicalLemmas.Geometry.LogConcavity.LogConcaveOn.mul · theorem · Teaching coverage

Statement

Let E be a real module and f,g:E→ℝ positive log-concave on the same set s⊆E. Then their pointwise product x↦f(x)g(x) is positive log-concave on s.

\[\operatorname{LC}_s(f),\operatorname{LC}_s(g)\Longrightarrow\operatorname{LC}_s(fg).\]

All objects and hypotheses

E : Type* with [AddCommMonoid E] and [Module ℝ E]. These are the exact algebraic ambient structures; no topology, norm, measure or finite-dimensionality is assumed.
s : Set E; f,g : E → ℝ; hf : LogConcaveOn s f and hg : LogConcaveOn s g.

{'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. Prove product positivity

At every point of s both factors are positive, so their product is positive.

\[f(x)>0,\ g(x)>0\Longrightarrow f(x)g(x)>0.\]

Corresponding Lean step

refine ⟨fun x hx => mul_pos (hf.pos (x := x) hx) (hg.pos (x := x) hx), ?_⟩

The two components requested here are the exact clauses of the predicate, not extra hypotheses.

2. Add the two concave logarithms

Adding their concavity inequalities proves that log f+log g is concave on the common convex domain.

\[a(\log f(x)+\log g(x))+b(\log f(y)+\log g(y))\le\log f(ax+by)+\log g(ax+by).\]

Corresponding Lean step

have hsum := hf.concaveOn_log.add hg.concaveOn_log

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

3. Identify the sum as the logarithm of the product

The factors are nonzero by positivity, so the logarithm product identity holds at each domain point. Replace the concave sum by log(fg) using equality on s.

\[\log(f(x)g(x))=\log f(x)+\log g(x)\quad(x\in s).\]

Corresponding Lean step

refine hsum.congr ?_
intro x hx
simpa using (Real.log_mul (hf.pos (x := x) hx).ne' (hg.pos (x := x) hx).ne').symm

The congr operation transfers the geometric property to a function equal on the domain; all needed log identities are justified at positive arguments.

Lean statement · mul

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. The pointwise product f*g is not a convolution. .ne' turns a strict positivity proof into the nonzero premise needed by log_mul; congr transfers concavity through pointwise equality.

theorem LogConcaveOn.mul {E : Type*} [AddCommMonoid E] [Module ℝ E]
    {s : Set E} {f g : E → ℝ}
    (hf : LogConcaveOn s f) (hg : LogConcaveOn s g) :
    LogConcaveOn s (fun x => f x * g x)

Exact module and namespace context

Lean proof · mul

The pointwise product f*g is not a convolution. .ne' turns a strict positivity proof into the nonzero premise needed by log_mul; congr transfers concavity through pointwise equality.

theorem LogConcaveOn.mul {E : Type*} [AddCommMonoid E] [Module ℝ E]
    {s : Set E} {f g : E → ℝ}
    (hf : LogConcaveOn s f) (hg : LogConcaveOn s g) :
    LogConcaveOn s (fun x => f x * g x) := by
  refine ⟨fun x hx => mul_pos (hf.pos (x := x) hx) (hg.pos (x := x) hx), ?_⟩
  have hsum :
      ConcaveOn ℝ s ((fun x => Real.log (f x)) + fun x => Real.log (g x)) :=
    hf.concaveOn_log.add hg.concaveOn_log
  refine hsum.congr ?_
  intro x hx
  simpa using (Real.log_mul (hf.pos (x := x) hx).ne' (hg.pos (x := x) hx).ne').symm

/-- A nonnegative real power of a positive log-concave function is log-concave. -/

Exact module and namespace context

Scope and omitted-condition boundaries

The product has not been normalized as a probability density; no integration is involved.
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)

mul_pos
ConcaveOn.add
ConcaveOn.congr
Real.log_mul

Mathematical sources

Existing ASTIS declaration and exact proof — Directly read current local source; no Lean edit or fresh build.
Existing curated module card — Local API/source-boundary memory; not independent primary textbook verification.
ConcaveOn.add — Exact inspected Mathlib definition or theorem used by this exposition.
ConcaveOn.congr — Exact inspected Mathlib definition or theorem used by this exposition.
Real.log_mul — Exact inspected Mathlib definition or theorem used by this exposition.
Existing usage in Tests.Basic — Read-only source example; no test was run.

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

ASTIS mathematical exposition

Nonnegative real powers preserve positive log-concavity

AutoSamplingTheory.TechnicalLemmas.Geometry.LogConcavity.LogConcaveOn.rpow · theorem · Teaching coverage

Statement

Let E be a real module, f:E→ℝ positive log-concave on s⊆E, and p≥0 a real number. Then x↦f(x)^p, with real exponentiation, is positive log-concave on s. The exponent zero is allowed.

\[\operatorname{LC}_s(f),\quad p\ge0\Longrightarrow\operatorname{LC}_s(f^p),\qquad\log(f(x)^p)=p\log f(x).\]

All objects and hypotheses

E : Type* with [AddCommMonoid E] and [Module ℝ E]. These are the exact algebraic ambient structures; no topology, norm, measure or finite-dimensionality is assumed.
s : Set E, f : E → ℝ, hf : LogConcaveOn s f.
p : ℝ and hp : 0≤p.

{'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. Real powers of positive numbers stay positive

Since f(x)>0 on s, its real power is positive for any real exponent, in particular the supplied p.

\[f(x)>0\Longrightarrow f(x)^p>0.\]

Corresponding Lean step

refine ⟨fun x hx => Real.rpow_pos_of_pos (hf.pos (x := x) hx) p, ?_⟩

The two components requested here are the exact clauses of the predicate, not extra hypotheses.

2. Scale the logarithmic concavity inequality by p

Because p is nonnegative, multiplying a concavity inequality by p keeps its direction. Thus p log f is concave on s.

\[a[p\log f(x)]+b[p\log f(y)]\le p\log f(ax+by).\]

Corresponding Lean step

have hscaled : ConcaveOn ℝ s (fun x => p • Real.log (f x)) := hf.concaveOn_log.smul hp

The .smul API scales an inequality; its nonnegative scalar hypothesis is what preserves the inequality direction.

3. Identify the logarithm of the real power

At positive arguments log(f(x)^p)=p log f(x). Replace the scaled function by this equal logarithm and combine with positivity.

\[\log(f^p)=p\log f\quad\text{on }s.\]

Corresponding Lean step

refine hscaled.congr ?_
intro x hx
simpa [smul_eq_mul] using (Real.log_rpow (hf.pos (x := x) hx) p).symm

The congr operation transfers the geometric property to a function equal on the domain; all needed log identities are justified at positive arguments.

Lean statement · rpow

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. p is a real number, so ^ uses real exponentiation here. Its nonnegative sign is needed to preserve concavity after scaling; it is not needed merely for positivity.

theorem LogConcaveOn.rpow {E : Type*} [AddCommMonoid E] [Module ℝ E]
    {s : Set E} {f : E → ℝ} {p : ℝ}
    (hf : LogConcaveOn s f) (hp : 0 ≤ p) :
    LogConcaveOn s (fun x => (f x) ^ p)

Exact module and namespace context

Lean proof · rpow

p is a real number, so ^ uses real exponentiation here. Its nonnegative sign is needed to preserve concavity after scaling; it is not needed merely for positivity.

theorem LogConcaveOn.rpow {E : Type*} [AddCommMonoid E] [Module ℝ E]
    {s : Set E} {f : E → ℝ} {p : ℝ}
    (hf : LogConcaveOn s f) (hp : 0 ≤ p) :
    LogConcaveOn s (fun x => (f x) ^ p) := by
  refine ⟨fun x hx => Real.rpow_pos_of_pos (hf.pos (x := x) hx) p, ?_⟩
  have hscaled : ConcaveOn ℝ s (fun x => p • Real.log (f x)) :=
    hf.concaveOn_log.smul hp
  refine hscaled.congr ?_
  intro x hx
  simpa [smul_eq_mul] using (Real.log_rpow (hf.pos (x := x) hx) p).symm

/-- Product-domain tensorization: the product of log-concave factors on
convex domains is log-concave on the Cartesian product. -/

Exact module and namespace context

Scope and omitted-condition boundaries

No conclusion for negative p is asserted; negative scaling generally changes concavity to convexity.
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.rpow_pos_of_pos
ConcaveOn.smul
ConcaveOn.congr
Real.log_rpow
smul_eq_mul

Mathematical sources

Existing ASTIS declaration and exact proof — Directly read current local source; no Lean edit or fresh build.
Existing curated module card — Local API/source-boundary memory; not independent primary textbook verification.
Real.rpow_pos_of_pos — Exact inspected Mathlib definition or theorem used by this exposition.
ConcaveOn.smul — Exact inspected Mathlib definition or theorem used by this exposition.
ConcaveOn.congr — Exact inspected Mathlib definition or theorem used by this exposition.
Real.log_rpow — Exact inspected Mathlib definition or theorem used by this exposition.
Existing usage in Tests.Basic — Read-only source example; no test was run.

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

ASTIS mathematical exposition

Tensor products are log-concave on product domains

AutoSamplingTheory.TechnicalLemmas.Geometry.LogConcavity.LogConcaveOn.prod · theorem · Teaching coverage

Statement

Let E,F be real modules, s⊆E, t⊆F, and f:E→ℝ and g:F→ℝ positive log-concave on s and t respectively. Then h(x,y)=f(x)g(y) is positive log-concave on s×t.

\[\operatorname{LC}_s(f),\operatorname{LC}_t(g)\Longrightarrow\operatorname{LC}_{s\times t}\bigl((x,y)\mapsto f(x)g(y)\bigr).\]

All objects and hypotheses

E,F : Type* with [AddCommMonoid E] [Module ℝ E] [AddCommMonoid F] [Module ℝ F]. No topological or measure structures are assumed.
s : Set E, t : Set F, f : E → ℝ, g : F → ℝ.
hf : LogConcaveOn s f; hg : LogConcaveOn t g.

{'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. Check positivity and the product domain

The two positive factors give a positive product at every (x,y)∈s×t. Since s and t are convex, combinations taken componentwise remain in s×t.

\[f(x)g(y)>0,\qquad a(u_1,u_2)+b(v_1,v_2)=(au_1+bv_1,au_2+bv_2)\in s\times t.\]

Corresponding Lean step

refine ⟨fun x hx => mul_pos (hf.pos (x := x.1) hx.1) (hg.pos (x := x.2) hx.2), ?_⟩
refine ⟨hf.convex_domain.prod hg.convex_domain, ?_⟩

The two components requested here are the exact clauses of the predicate, not extra hypotheses.

2. Apply concavity to each coordinate separately

For u,v∈s×t and a,b≥0 summing to one, apply the f inequality to u₁,v₁ and the g inequality to u₂,v₂. Add them.

\[a\log f(u_1)+b\log f(v_1)+a\log g(u_2)+b\log g(v_2)\le\log f(au_1+bv_1)+\log g(au_2+bv_2).\]

Corresponding Lean step

have hF := hf.concaveOn_log.2 hx.1 hy.1 ha hb hab
have hG := hg.concaveOn_log.2 hx.2 hy.2 ha hb hab
have hsum := add_le_add hF hG

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

3. Rewrite both sides as product logarithms

At the endpoints and their convex combination all factors are positive. Use log(fg)=log f+log g, distribute the weights, and regroup the terms. The inequality from the previous step becomes the concavity inequality for log h.

\[a\log h(u)+b\log h(v)\le\log h(au+bv).\]

Corresponding Lean step

have hmid := (hf.convex_domain.prod hg.convex_domain) hx hy ha hb hab
-- The calc block applies Real.log_mul at x, y and the midpoint; simp [smul_eq_mul] and ring regroup; its inequality is hsum.

hmid records domain membership of the convex combination, permitting the same positivity assumptions at that point.

Lean statement · prod

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. The two component spaces may differ. x.1 and x.2 access their coordinates. The proof establishes a product-domain result directly, rather than appealing to a probability independence or marginalization theorem.

theorem LogConcaveOn.prod {E F : Type*}
    [AddCommMonoid E] [Module ℝ E] [AddCommMonoid F] [Module ℝ F]
    {s : Set E} {t : Set F} {f : E → ℝ} {g : F → ℝ}
    (hf : LogConcaveOn s f) (hg : LogConcaveOn t g) :
    LogConcaveOn (s ×ˢ t) (fun x : E × F => f x.1 * g x.2)

Exact module and namespace context

Lean proof · prod

The two component spaces may differ. x.1 and x.2 access their coordinates. The proof establishes a product-domain result directly, rather than appealing to a probability independence or marginalization theorem.

theorem LogConcaveOn.prod {E F : Type*}
    [AddCommMonoid E] [Module ℝ E] [AddCommMonoid F] [Module ℝ F]
    {s : Set E} {t : Set F} {f : E → ℝ} {g : F → ℝ}
    (hf : LogConcaveOn s f) (hg : LogConcaveOn t g) :
    LogConcaveOn (s ×ˢ t) (fun x : E × F => f x.1 * g x.2) := by
  refine ⟨fun x hx => mul_pos (hf.pos (x := x.1) hx.1) (hg.pos (x := x.2) hx.2), ?_⟩
  refine ⟨hf.convex_domain.prod hg.convex_domain, ?_⟩
  intro x hx y hy a b ha hb hab
  have hF := hf.concaveOn_log.2 hx.1 hy.1 ha hb hab
  have hG := hg.concaveOn_log.2 hx.2 hy.2 ha hb hab
  have hsum := add_le_add hF hG
  have hmid : a • x + b • y ∈ s ×ˢ t :=
    (hf.convex_domain.prod hg.convex_domain) hx hy ha hb hab
  calc
    a • Real.log (f x.1 * g x.2) + b • Real.log (f y.1 * g y.2)
        = (a • Real.log (f x.1) + b • Real.log (f y.1)) +
            (a • Real.log (g x.2) + b • Real.log (g y.2)) := by
          rw [Real.log_mul (hf.pos (x := x.1) hx.1).ne' (hg.pos (x := x.2) hx.2).ne',
            Real.log_mul (hf.pos (x := y.1) hy.1).ne' (hg.pos (x := y.2) hy.2).ne']
          simp [smul_eq_mul]
          ring
    _ ≤ Real.log (f (a • x.1 + b • y.1)) + Real.log (g (a • x.2 + b • y.2)) := hsum
    _ = Real.log (f (a • x.1 + b • y.1) * g (a • x.2 + b • y.2)) := by
          rw [Real.log_mul (hf.pos (x := a • x.1 + b • y.1) hmid.1).ne'
            (hg.pos (x := a • x.2 + b • y.2) hmid.2).ne']
    _ = Real.log (f (a • x + b • y).1 * g (a • x + b • y).2) := by simp

/-- Multiplication by a positive constant preserves log-concavity. -/

Exact module and namespace context

Scope and omitted-condition boundaries

This is a product of function values on a Cartesian product, not a convolution or Prékopa–Leindler theorem.
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)

Convex.prod
mul_pos
add_le_add
Real.log_mul
smul_eq_mul

Mathematical sources

Existing ASTIS declaration and exact proof — Directly read current local source; no Lean edit or fresh build.
Existing curated module card — Local API/source-boundary memory; not independent primary textbook verification.
Convex.prod — Exact inspected Mathlib definition or theorem used by this exposition.
Real.log_mul — Exact inspected Mathlib definition or theorem used by this exposition.
Existing usage in Tests.Basic — Read-only source example; no test was run.

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

ASTIS mathematical exposition

Positive rescaling preserves log-concavity

AutoSamplingTheory.TechnicalLemmas.Geometry.LogConcavity.LogConcaveOn.const_mul · theorem · Teaching coverage

Statement

Let E be a real module, f:E→ℝ positive log-concave on s⊆E, and c>0 a real constant. Then x↦c f(x) is positive log-concave on s.

\[c>0,\quad\operatorname{LC}_s(f)\Longrightarrow\operatorname{LC}_s(cf),\qquad \log(cf)=\log c+\log f.\]

All objects and hypotheses

E : Type* with [AddCommMonoid E] and [Module ℝ E]. These are the exact algebraic ambient structures; no topology, norm, measure or finite-dimensionality is assumed.
s : Set E, f : E → ℝ, hf : LogConcaveOn s f.
c : ℝ and hc : 0<c.

{'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. Keep strict positivity

Multiplying two positive real numbers leaves a positive number, so cf is positive on s.

\[c>0,\ f(x)>0\Longrightarrow cf(x)>0.\]

Corresponding Lean step

refine ⟨fun x hx => mul_pos hc (hf.pos (x := x) hx), ?_⟩

The two components requested here are the exact clauses of the predicate, not extra hypotheses.

2. Add a constant to the concave logarithm

The constant function log c is concave on the convex domain s: every weighted average of its values equals itself. Adding it to log f preserves concavity.

\[a\log c+b\log c=(a+b)\log c=\log c,\qquad \log c+\log f\text{ concave on }s.\]

Corresponding Lean step

have hconst := concaveOn_const (Real.log c) hf.convex_domain
have hsum := hconst.add hf.concaveOn_log

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

3. Recognize the logarithm of the rescaled function

Positivity supplies the nonzero premises of log_mul. Replace log c+log f(x) by log(c f(x)) on s, obtaining the required concavity.

\[\log(cf(x))=\log c+\log f(x).\]

Corresponding Lean step

refine hsum.congr ?_
intro x hx
simpa using (Real.log_mul hc.ne' (hf.pos (x := x) hx).ne').symm

The congr operation transfers the geometric property to a function equal on the domain; all needed log identities are justified at positive arguments.

Lean statement · const_mul

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. c is constant in x. The strict inequality hc is essential for this positive-function convention; multiplying by zero would not preserve positivity on a nonempty domain.

theorem LogConcaveOn.const_mul {E : Type*} [AddCommMonoid E] [Module ℝ E]
    {s : Set E} {f : E → ℝ}
    (hf : LogConcaveOn s f) {c : ℝ} (hc : 0 < c) :
    LogConcaveOn s (fun x => c * f x)

Exact module and namespace context

Lean proof · const_mul

c is constant in x. The strict inequality hc is essential for this positive-function convention; multiplying by zero would not preserve positivity on a nonempty domain.

theorem LogConcaveOn.const_mul {E : Type*} [AddCommMonoid E] [Module ℝ E]
    {s : Set E} {f : E → ℝ}
    (hf : LogConcaveOn s f) {c : ℝ} (hc : 0 < c) :
    LogConcaveOn s (fun x => c * f x) := by
  refine ⟨fun x hx => mul_pos hc (hf.pos (x := x) hx), ?_⟩
  have hconst : ConcaveOn ℝ s (fun _ : E => Real.log c) :=
    concaveOn_const (Real.log c) hf.convex_domain
  have hsum :
      ConcaveOn ℝ s ((fun _ : E => Real.log c) + fun x => Real.log (f x)) :=
    hconst.add hf.concaveOn_log
  refine hsum.congr ?_
  intro x hx
  simpa using (Real.log_mul hc.ne' (hf.pos (x := x) hx).ne').symm

/-- A positive constant function is log-concave on every convex domain. -/

Exact module and namespace context

Scope and omitted-condition boundaries

An arbitrary positive rescaling is not automatically a probability normalization.
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)

mul_pos
concaveOn_const
ConcaveOn.add
ConcaveOn.congr
Real.log_mul

Mathematical sources

Existing ASTIS declaration and exact proof — Directly read current local source; no Lean edit or fresh build.
Existing curated module card — Local API/source-boundary memory; not independent primary textbook verification.
concaveOn_const — Exact inspected Mathlib definition or theorem used by this exposition.
ConcaveOn.add — Exact inspected Mathlib definition or theorem used by this exposition.
ConcaveOn.congr — Exact inspected Mathlib definition or theorem used by this exposition.
Real.log_mul — Exact inspected Mathlib definition or theorem used by this exposition.

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

ASTIS mathematical exposition

Positive constants are log-concave on convex domains

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

Statement

Let E be a real module, s⊆E a convex set, and c>0 a real number. The constant function x↦c is positive log-concave on s.

\[c>0,\quad s\text{ convex}\Longrightarrow\operatorname{LC}_s(x\mapsto c).\]

All objects and hypotheses

E : Type* with [AddCommMonoid E] and [Module ℝ E]. These are the exact algebraic ambient structures; no topology, norm, measure or finite-dimensionality is assumed.
s : Set E; c : ℝ; hc : 0<c; hs : Convex ℝ s.

{'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. Check the two constant-function clauses

Every function value is the supplied positive c. Its logarithm is constant log c, whose concavity inequality is equality because the weights sum to one; the domain is convex by hs.

\[c>0,\qquad a\log c+b\log c=\log c\quad(a+b=1).\]

Corresponding Lean step

⟨fun _ _ => hc, concaveOn_const (Real.log c) hs⟩

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_const

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. Both the positive value and convex domain are explicit inputs. A constant function need not integrate to a finite mass on an infinite-volume domain.

theorem logConcaveOn_const {E : Type*} [AddCommMonoid E] [Module ℝ E]
    {s : Set E} {c : ℝ} (hc : 0 < c) (hs : Convex ℝ s) :
    LogConcaveOn s (fun _ : E => c)

Exact module and namespace context

Lean proof · logConcaveOn_const

Both the positive value and convex domain are explicit inputs. A constant function need not integrate to a finite mass on an infinite-volume domain.

theorem logConcaveOn_const {E : Type*} [AddCommMonoid E] [Module ℝ E]
    {s : Set E} {c : ℝ} (hc : 0 < c) (hs : Convex ℝ s) :
    LogConcaveOn s (fun _ : E => c) :=
  ⟨fun _ _ => hc, concaveOn_const (Real.log c) hs⟩

/-- If `V` is convex, then the unnormalized Gibbs shape `exp (-V)` is
log-concave. -/

Exact module and namespace context

Scope and omitted-condition boundaries

No measure or normalizing claim.
This documentation adds no Lean theorem, compilation evidence, source-equivalence verdict, or new source-fidelity certification.

Source and reuse

ASTIS parents called

AutoSamplingTheory.TechnicalLemmas.Geometry.LogConcavity.LogConcaveOn

Mathlib API called (external library)

concaveOn_const

Mathematical sources

Existing ASTIS declaration and exact proof — Directly read current local source; no Lean edit or fresh build.
Existing curated module card — Local API/source-boundary memory; not independent primary textbook verification.
concaveOn_const — Exact inspected Mathlib definition or theorem used by this exposition.

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

ASTIS mathematical exposition

A convex potential gives a log-concave Gibbs shape

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

Statement

Let E be a real module, s⊆E, and V:E→ℝ convex on s. Then x↦exp(−V(x)) is positive log-concave on s.

\[\operatorname{Convex}_s(V)\Longrightarrow\operatorname{LC}_s(e^{-V}),\qquad\log(e^{-V(x)})=-V(x).\]

All objects and hypotheses

E : Type* with [AddCommMonoid E] and [Module ℝ E]. These are the exact algebraic ambient structures; no topology, norm, measure or finite-dimensionality is assumed.
s : Set E, V : E → ℝ, hV : ConvexOn ℝ s V; this includes convexity of s.

{'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. Exponential values are strictly positive

The real exponential is positive at every real argument, so exp(−V(x)) is positive on s without any lower or upper bound on V.

\[\exp(-V(x))>0.\]

Corresponding Lean step

refine ⟨fun _ _ => Real.exp_pos _, ?_⟩

The two components requested here are the exact clauses of the predicate, not extra hypotheses.

2. Identify the logarithm and negate convexity

Negating the convexity inequality for V makes −V concave. Since log(exp(−V(x)))=−V(x), this is exactly concavity of the logarithm of the Gibbs shape.

\[V(ax+by)\le aV(x)+bV(y)\Longrightarrow a[-V(x)]+b[-V(y)]\le -V(ax+by)=\log(e^{-V(ax+by)}).\]

Corresponding Lean step

exact hV.neg.congr fun _ _ => by simp

The congr operation transfers the geometric property to a function equal on the domain; all needed log identities are justified at positive arguments.

Lean statement · logConcaveOn_exp_neg_of_convexOn

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. hV.neg reuses the sign-reversal theorem; congr replaces equal functions on s, using log_exp. The exponential is a shape function, not yet a probability density.

theorem logConcaveOn_exp_neg_of_convexOn {E : Type*} [AddCommMonoid E] [Module ℝ E]
    {s : Set E} {V : E → ℝ} (hV : ConvexOn ℝ s V) :
    LogConcaveOn s (fun x => Real.exp (-V x))

Exact module and namespace context

Lean proof · logConcaveOn_exp_neg_of_convexOn

hV.neg reuses the sign-reversal theorem; congr replaces equal functions on s, using log_exp. The exponential is a shape function, not yet a probability density.

theorem logConcaveOn_exp_neg_of_convexOn {E : Type*} [AddCommMonoid E] [Module ℝ E]
    {s : Set E} {V : E → ℝ} (hV : ConvexOn ℝ s V) :
    LogConcaveOn s (fun x => Real.exp (-V x)) := by
  refine ⟨fun _ _ => Real.exp_pos _, ?_⟩
  exact hV.neg.congr fun _ _ => by simp

/-- A positive multiple of the Gibbs shape of a convex potential is
log-concave.  This is the convex-analytic part of normalized Gibbs-density
bookkeeping; the measure/integral normalization proof is a separate leaf. -/

Exact module and namespace context

Scope and omitted-condition boundaries

Integrability, a positive finite partition function, normalization and sampling are not conclusions.
This documentation adds no Lean theorem, compilation evidence, source-equivalence verdict, or new source-fidelity certification.

Source and reuse

ASTIS parents called

AutoSamplingTheory.TechnicalLemmas.Geometry.LogConcavity.LogConcaveOn

Mathlib API called (external library)

Real.exp_pos
ConvexOn.neg
ConcaveOn.congr
Real.log_exp

Mathematical sources

Existing ASTIS declaration and exact proof — Directly read current local source; no Lean edit or fresh build.
Existing curated module card — Local API/source-boundary memory; not independent primary textbook verification.
ConvexOn.neg — Exact inspected Mathlib definition or theorem used by this exposition.
ConcaveOn.congr — Exact inspected Mathlib definition or theorem used by this exposition.
Real.log_exp — Exact inspected Mathlib definition or theorem used by this exposition.
Real.exp_pos — Exact local Mathlib declaration anchor.

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

ASTIS mathematical exposition

A positively rescaled convex-potential Gibbs shape is log-concave

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

Statement

Let E be a real module, s⊆E, V:E→ℝ convex on s, and c>0 a real constant. Then x↦c exp(−V(x)) is positive log-concave on s.

\[\operatorname{Convex}_s(V),\quad c>0\Longrightarrow\operatorname{LC}_s(ce^{-V}).\]

All objects and hypotheses

E : Type* with [AddCommMonoid E] and [Module ℝ E]. These are the exact algebraic ambient structures; no topology, norm, measure or finite-dimensionality is assumed.
s : Set E, V : E → ℝ, hV : ConvexOn ℝ s V.
c : ℝ, hc : 0<c.

{'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. Apply the convex-potential result

The existing theorem proves positivity and log-concavity of exp(−V) on s from the supplied convexity.

\[\operatorname{Convex}_s(V)\Longrightarrow\operatorname{LC}_s(e^{-V}).\]

Corresponding Lean step

logConcaveOn_exp_neg_of_convexOn hV

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

2. Rescale by the positive constant

Apply positive-rescaling closure to c. Equivalently, the new logarithm is log c−V, a concave function obtained by a constant shift.

\[\log(ce^{-V})=\log c-V,\qquad ce^{-V}>0.\]

Corresponding Lean step

(logConcaveOn_exp_neg_of_convexOn hV).const_mul hc

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_const_mul_exp_neg_of_convexOn

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. This proof composes two existing results. c may later be chosen as a partition-function reciprocal, but the declaration assumes only c>0.

theorem logConcaveOn_const_mul_exp_neg_of_convexOn {E : Type*}
    [AddCommMonoid E] [Module ℝ E]
    {s : Set E} {V : E → ℝ} {c : ℝ}
    (hV : ConvexOn ℝ s V) (hc : 0 < c) :
    LogConcaveOn s (fun x => c * Real.exp (-V x))

Exact module and namespace context

Lean proof · logConcaveOn_const_mul_exp_neg_of_convexOn

This proof composes two existing results. c may later be chosen as a partition-function reciprocal, but the declaration assumes only c>0.

theorem logConcaveOn_const_mul_exp_neg_of_convexOn {E : Type*}
    [AddCommMonoid E] [Module ℝ E]
    {s : Set E} {V : E → ℝ} {c : ℝ}
    (hV : ConvexOn ℝ s V) (hc : 0 < c) :
    LogConcaveOn s (fun x => c * Real.exp (-V x)) :=
  (logConcaveOn_exp_neg_of_convexOn hV).const_mul hc

/-- The absolute value is convex on the real line. -/

Exact module and namespace context

Scope and omitted-condition boundaries

Reuse/integration wrapper; no assertion that c normalizes an integral.
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)

No direct Mathlib call recorded; see the ASTIS parents.

Mathematical sources

Existing ASTIS declaration and exact proof — Directly read current local source; no Lean edit or fresh build.
Existing curated module card — Local API/source-boundary memory; not independent primary textbook verification.
Existing usage in Tests.Basic — Read-only source example; no test was run.

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

ASTIS mathematical exposition

Absolute value is convex on the real line

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

Statement

The function x↦|x| is convex on all of ℝ: for any real x,y and any nonnegative real weights λ,θ summing to one, |λx+θy|≤λ|x|+θ|y|.

\[\operatorname{Convex}_{\mathbb R}(x\mapsto|x|),\qquad|\lambda x+\theta y|\le\lambda|x|+\theta|y|\quad(\lambda,\theta\ge0,\ \lambda+\theta=1).\]

All objects and hypotheses

The ambient scalar field and state space are ℝ with their usual additive/module structures.
There are no explicit parameters or hypotheses; the ambient space and scalars are ℝ.

{'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. Identify absolute value with the real norm

For a real number, its norm is its absolute value. Thus the requested function is exactly the norm on the real normed vector space ℝ.

\[|x|=\|x\|_{\mathbb R}.\]

Corresponding Lean step

change ConvexOn ℝ Set.univ (norm : ℝ → ℝ)

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 norm convexity

The norm triangle inequality and homogeneity give ‖λx+θy‖≤‖λx‖+‖θy‖=λ‖x‖+θ‖y‖ for nonnegative weights. The whole real line is convex, so Mathlib's norm-convexity theorem proves the result.

\[|\lambda x+\theta y|\le|\lambda x|+|\theta y|=\lambda|x|+\theta|y|.\]

Corresponding Lean step

exact convexOn_univ_norm

The final call supplies the named existing result after matching its parameters with this statement.

Lean statement · convexOn_univ_abs

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. change only rewrites the real absolute-value function as the equal norm function. The existing norm theorem supplies the complete convexity proof.

theorem convexOn_univ_abs :
    ConvexOn ℝ (Set.univ : Set ℝ) (fun x : ℝ => |x|)

Exact module and namespace context

Lean proof · convexOn_univ_abs

change only rewrites the real absolute-value function as the equal norm function. The existing norm theorem supplies the complete convexity proof.

theorem convexOn_univ_abs :
    ConvexOn ℝ (Set.univ : Set ℝ) (fun x : ℝ => |x|) := by
  change ConvexOn ℝ Set.univ (norm : ℝ → ℝ)
  exact convexOn_univ_norm

/-- Nonnegative absolute-linear real potentials are convex. -/

Exact module and namespace context

Scope and omitted-condition boundaries

This is convexity, not differentiability at the origin or strict convexity.
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)

convexOn_univ_norm

Mathematical sources

Existing ASTIS declaration and exact proof — Directly read current local source; no Lean edit or fresh build.
Existing curated module card — Local API/source-boundary memory; not independent primary textbook verification.
convexOn_univ_norm — Exact inspected Mathlib definition or theorem used by this exposition.
Existing usage in Tests.Basic — Read-only source example; no test was run.

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

ASTIS mathematical exposition

Convexity of a absolute-linear potential

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

Statement

On the real line ℝ, let a,b∈ℝ with a≥0. Then V=a|x|+b is convex on the entire space. There is no sign restriction on b.

\[V=a|x|+b,\qquad\operatorname{Convex}_{ℝ}(V)\quad(a\ge0).\]

All objects and hypotheses

The ambient scalar field and state space are ℝ with their usual additive/module structures.
a,b : ℝ; ha : 0≤a; b is 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. Start with the convex base function

The existing absolute-value theorem gives convexity of U(x)=|x| on the whole space.

\[U(\lambda x+\theta y)\le\lambda U(x)+\theta U(y).\]

Corresponding Lean step

convexOn_univ_abs

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

2. Multiply by a nonnegative coefficient

Since a≥0, multiplying the convexity inequality by a preserves its direction. This proves convexity of aU.

\[aU(\lambda x+\theta y)\le\lambda aU(x)+\theta aU(y).\]

Corresponding Lean step

have h := convexOn_univ_abs.smul ha

The .smul API scales an inequality; its nonnegative scalar hypothesis is what preserves the inequality direction.

3. Add the constant offset

Add b to both sides and use λ+θ=1 to distribute b as λb+θb. The result is the convexity inequality for V=aU+b.

\[aU(\lambda x+\theta y)+b\le\lambda(aU(x)+b)+\theta(aU(y)+b).\]

Corresponding Lean step

simpa only [smul_eq_mul] using h.add_const b

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 · convexOn_univ_const_mul_abs_add

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. This declaration proves a convexity property of a real-valued potential. Its nonnegative scaling and constant addition is the exact transformation used in the source, rather than a Hessian argument requiring extra smoothness.

theorem convexOn_univ_const_mul_abs_add {a b : ℝ} (ha : 0 ≤ a) :
    ConvexOn ℝ (Set.univ : Set ℝ) (fun x : ℝ => a * |x| + b)

Exact module and namespace context

Lean proof · convexOn_univ_const_mul_abs_add

This declaration proves a convexity property of a real-valued potential. Its nonnegative scaling and constant addition is the exact transformation used in the source, rather than a Hessian argument requiring extra smoothness.

theorem convexOn_univ_const_mul_abs_add {a b : ℝ} (ha : 0 ≤ a) :
    ConvexOn ℝ (Set.univ : Set ℝ) (fun x : ℝ => a * |x| + b) := by
  have h := convexOn_univ_abs.smul ha
  change ConvexOn ℝ Set.univ ((fun x : ℝ => a * |x|) + fun _ => b)
  simpa only [smul_eq_mul] using h.add_const b

/-- The Gibbs shape of a nonnegative absolute-linear real potential is
log-concave. -/

Exact module and namespace context

Scope and omitted-condition boundaries

Only convexity is established. Coefficient a=0 is allowed; strong convexity, coercivity and integrability do not follow from this result.
This documentation adds no Lean theorem, compilation evidence, source-equivalence verdict, or new source-fidelity certification.

Source and reuse

ASTIS parents called

AutoSamplingTheory.TechnicalLemmas.Geometry.LogConcavity.convexOn_univ_abs

Mathlib API called (external library)

ConvexOn.smul
ConvexOn.add_const
smul_eq_mul

Mathematical sources

Existing ASTIS declaration and exact proof — Directly read current local source; no Lean edit or fresh build.
Existing curated module card — Local API/source-boundary memory; not independent primary textbook verification.
ConvexOn.smul — Exact inspected Mathlib definition or theorem used by this exposition.
ConvexOn.add_const — Exact inspected Mathlib definition or theorem used by this exposition.
Existing usage in Tests.Basic — Read-only source example; no test was run.

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

ASTIS mathematical exposition

Log-concavity of a absolute-linear Gibbs shape

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

Statement

On the real line ℝ, let a,b∈ℝ with a≥0. For the potential V=a|x|+b, the function exp(−V) is strictly positive and log-concave on the whole space.

\[V=a|x|+b,\qquad\operatorname{LC}_{ℝ}(e^{-V})\quad(a\ge0).\]

All objects and hypotheses

The ambient scalar field and state space are ℝ with their usual additive/module structures.
a,b : ℝ; ha : 0≤a; no sign condition on b.

{'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. Supply the already-proved convex potential

The corresponding potential theorem establishes convexity of V with exactly the supplied a≥0 and the same unrestricted b.

\[\operatorname{Convex}_{ℝ}(V).\]

Corresponding Lean step

convexOn_univ_const_mul_abs_add (a := a) (b := b) ha

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

2. Use exponential positivity and the log identity

The generic convex-potential theorem says exp(−V)>0 and log(exp(−V))=−V. Negating the convex potential gives a concave logarithm, so the theorem applies directly.

\[e^{-V}>0,\qquad\log(e^{-V})=-V\text{ is concave}.\]

Corresponding Lean step

simpa using logConcaveOn_exp_neg_of_convexOn
  (convexOn_univ_const_mul_abs_add (a := a) (b := b) ha)

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_exp_neg_abs_linear

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. simpa only aligns the specialized formula with the generic Gibbs-shape theorem. The argument is reuse of the convex-potential result, not a new integration or differential calculation.

theorem logConcaveOn_exp_neg_abs_linear {a b : ℝ} (ha : 0 ≤ a) :
    LogConcavity.LogConcaveOn (Set.univ : Set ℝ)
      (fun x : ℝ => Real.exp (-(a * |x| + b)))

Exact module and namespace context

Lean proof · logConcaveOn_exp_neg_abs_linear

simpa only aligns the specialized formula with the generic Gibbs-shape theorem. The argument is reuse of the convex-potential result, not a new integration or differential calculation.

theorem logConcaveOn_exp_neg_abs_linear {a b : ℝ} (ha : 0 ≤ a) :
    LogConcavity.LogConcaveOn (Set.univ : Set ℝ)
      (fun x : ℝ => Real.exp (-(a * |x| + b))) := by
  simpa using logConcaveOn_exp_neg_of_convexOn
    (convexOn_univ_const_mul_abs_add (a := a) (b := b) ha)

/-- Positive scalar normalization preserves log-concavity of absolute-linear
Laplace shapes. -/

Exact module and namespace context

Scope and omitted-condition boundaries

The conclusion is log-concavity of a function shape. No normalizing integral, probability law or executable kernel is constructed.
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)

No direct Mathlib call recorded; see the ASTIS parents.

Mathematical sources

Existing ASTIS declaration and exact proof — Directly read current local source; no Lean edit or fresh build.
Existing curated module card — Local API/source-boundary memory; not independent primary textbook verification.
Existing usage in Tests.Basic — Read-only source example; no test was run.

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

ASTIS mathematical exposition

Positive rescaling of the absolute-linear Gibbs shape

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

Statement

On the real line ℝ, let a,b,c∈ℝ with a≥0 and c>0. With V=a|x|+b, the function c exp(−V) is positive log-concave on the whole domain. The constant c is not required or proved to normalize an integral.

\[V=a|x|+b,\qquad a\ge0,\ c>0\Longrightarrow\operatorname{LC}_{ℝ}(ce^{-V}).\]

All objects and hypotheses

The ambient scalar field and state space are ℝ with their usual additive/module structures.
a,b : ℝ; ha : 0≤a; no sign condition on b.
c : ℝ; hc : 0<c.

{'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. Verify the potential's convexity

Reuse the corresponding convexity theorem for V; it requires a≥0 and imposes no bound on b.

\[\operatorname{Convex}_{ℝ}(V).\]

Corresponding Lean step

convexOn_univ_const_mul_abs_add (a := a) (b := b) ha

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

2. Apply the positive-rescaled Gibbs-shape theorem

For any positive c, log(c exp(−V))=log c−V is concave and the function itself is positive. Apply the generic result to the verified V and the supplied c>0.

\[\log(ce^{-V})=\log c-V,\qquad ce^{-V}>0.\]

Corresponding Lean step

simpa using logConcaveOn_const_mul_exp_neg_of_convexOn
  (convexOn_univ_const_mul_abs_add (a := a) (b := b) ha) hc

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_const_mul_exp_neg_abs_linear

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. There are two sign assumptions with different roles: ha lets the potential be convex, and hc keeps the rescaled function strictly positive. The theorem accepts any such c.

theorem logConcaveOn_const_mul_exp_neg_abs_linear {a b c : ℝ}
    (ha : 0 ≤ a) (hc : 0 < c) :
    LogConcavity.LogConcaveOn (Set.univ : Set ℝ)
      (fun x : ℝ => c * Real.exp (-(a * |x| + b)))

Exact module and namespace context

Lean proof · logConcaveOn_const_mul_exp_neg_abs_linear

There are two sign assumptions with different roles: ha lets the potential be convex, and hc keeps the rescaled function strictly positive. The theorem accepts any such c.

theorem logConcaveOn_const_mul_exp_neg_abs_linear {a b c : ℝ}
    (ha : 0 ≤ a) (hc : 0 < c) :
    LogConcavity.LogConcaveOn (Set.univ : Set ℝ)
      (fun x : ℝ => c * Real.exp (-(a * |x| + b))) := by
  simpa using logConcaveOn_const_mul_exp_neg_of_convexOn
    (convexOn_univ_const_mul_abs_add (a := a) (b := b) ha) hc

/-- The explicitly normalized one-dimensional absolute-linear Laplace density
is log-concave as a real-valued density shape. -/

Exact module and namespace context

Scope and omitted-condition boundaries

Positive rescaling does not certify a partition function or total mass one.
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)

No direct Mathlib call recorded; see the ASTIS parents.

Mathematical sources

Existing ASTIS declaration and exact proof — Directly read current local source; no Lean edit or fresh build.
Existing curated module card — Local API/source-boundary memory; not independent primary textbook verification.
Existing usage in Tests.Basic — Read-only source example; no test was run.

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

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.

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.

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

AutoSamplingTheory.TechnicalLemmas.Geometry.LogConcavity.logConcaveOn_const_mul_exp_neg_abs_linear

Mathlib API called (external library)

Real.exp_pos
inv_pos

Mathematical sources

Existing ASTIS declaration and exact proof — Directly read current local source; no Lean edit or fresh build.
Existing curated module card — Local API/source-boundary memory; not independent primary textbook verification.
Existing usage in Tests.Basic — Read-only source example; no test was run.
Real.exp_pos — Exact local Mathlib declaration anchor.

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

ASTIS mathematical exposition

Squared norms are convex on real normed spaces

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

Statement

Let E be any real normed vector space; finite dimension, completeness, an inner product and strict convexity of the norm are not assumed. Then x↦‖x‖² is convex on all of E.

\[\|\lambda x+\theta y\|^2\le\lambda\|x\|^2+\theta\|y\|^2\qquad(x,y\in E,\ \lambda,\theta\ge0,\ \lambda+\theta=1).\]

All objects and hypotheses

E : Type* with [NormedAddCommGroup E] and [NormedSpace ℝ E]. No finite-dimensionality, completeness or inner-product structure is required.
No hypotheses besides the ambient normed real vector-space structures. The proof considers arbitrary x,y and λ,θ≥0 with λ+θ=1.

{'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. The whole domain is convex

The domain is E itself, so every convex combination stays in it. Only the function inequality remains.

\[\lambda x+\theta y\in E.\]

Corresponding Lean step

refine ⟨convex_univ, ?_⟩
intro x _ y _ a b ha hb hab

The two components requested here are the exact clauses of the predicate, not extra hypotheses.

2. Bound the norm of a convex combination

Use the triangle inequality followed by norm homogeneity. Nonnegative weights have absolute value equal to themselves, yielding an upper bound L=λ‖x‖+θ‖y‖.

\[\|\lambda x+\theta y\|\le\|\lambda x\|+\|\theta y\|=\lambda\|x\|+\theta\|y\|=:L.\]

Corresponding Lean step

have hnorm : ‖a • x + b • y‖ ≤ a * ‖x‖ + b * ‖y‖ := by
  calc
    ‖a • x + b • y‖ ≤ ‖a • x‖ + ‖b • y‖ := norm_add_le _ _
    _ = a * ‖x‖ + b * ‖y‖ := by
      rw [norm_smul, norm_smul, Real.norm_of_nonneg ha, Real.norm_of_nonneg hb]

The rewrites identify equal expressions in the displayed mathematical calculation; they do not introduce extra assumptions.

3. Square the inequality using nonnegativity

Both the norm and L are nonnegative. Squaring is order-preserving on nonnegative reals, so the squared norm is at most L².

\[0\le\|\lambda x+\theta y\|\le L\Longrightarrow\|\lambda x+\theta y\|^2\le L^2.\]

Corresponding Lean step

have hnonneg := add_nonneg (mul_nonneg ha (norm_nonneg _)) (mul_nonneg hb (norm_nonneg _))
have hsq := (sq_le_sq₀ (norm_nonneg _) hnonneg).2 hnorm

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

4. Bound the square of the scalar weighted average

With u=‖x‖ and v=‖y‖, the condition λ+θ=1 gives an exact difference identity. Its right side is nonnegative, so L²≤λu²+θv². The code proves this identity algebraically; it does not assume convexity of the squared norm being established.

\[\lambda u^2+\theta v^2-(\lambda u+\theta v)^2=\lambda\theta(u-v)^2\ge0.\]

Corresponding Lean step

have hdiff_nonneg := mul_nonneg (mul_nonneg ha hb) (sq_nonneg (‖x‖ - ‖y‖))
-- hident proves the displayed equality by nlinarith [hab]; hjensen follows by nlinarith.

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

5. Combine the two bounds

Transitivity of the squared-norm bound and the scalar weighted-square bound gives precisely the convexity inequality.

\[\|\lambda x+\theta y\|^2\le L^2\le\lambda\|x\|^2+\theta\|y\|^2.\]

Corresponding Lean step

exact hsq.trans hjensen

The final call supplies the named existing result after matching its parameters with this statement.

Lean statement · convexOn_univ_norm_sq

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. The Lean proof uses a and b for the weights called λ and θ here. hnorm, hsq and hjensen are the three successive numerical bounds. nlinarith checks the scalar identity under a+b=1; the mathematical reason is the nonnegative term ab(‖x‖−‖y‖)².

theorem convexOn_univ_norm_sq {E : Type*} [NormedAddCommGroup E] [NormedSpace ℝ E] :
    ConvexOn ℝ (Set.univ : Set E) (fun x : E => ‖x‖ ^ 2)

Exact module and namespace context

Lean proof · convexOn_univ_norm_sq

The Lean proof uses a and b for the weights called λ and θ here. hnorm, hsq and hjensen are the three successive numerical bounds. nlinarith checks the scalar identity under a+b=1; the mathematical reason is the nonnegative term ab(‖x‖−‖y‖)².

theorem convexOn_univ_norm_sq {E : Type*} [NormedAddCommGroup E] [NormedSpace ℝ E] :
    ConvexOn ℝ (Set.univ : Set E) (fun x : E => ‖x‖ ^ 2) := by
  refine ⟨convex_univ, ?_⟩
  intro x _ y _ a b ha hb hab
  have hnorm : ‖a • x + b • y‖ ≤ a * ‖x‖ + b * ‖y‖ := by
    calc
      ‖a • x + b • y‖ ≤ ‖a • x‖ + ‖b • y‖ := norm_add_le _ _
      _ = a * ‖x‖ + b * ‖y‖ := by
        rw [norm_smul, norm_smul, Real.norm_of_nonneg ha, Real.norm_of_nonneg hb]
  have hnonneg : 0 ≤ a * ‖x‖ + b * ‖y‖ :=
    add_nonneg (mul_nonneg ha (norm_nonneg _)) (mul_nonneg hb (norm_nonneg _))
  have hsq : ‖a • x + b • y‖ ^ 2 ≤ (a * ‖x‖ + b * ‖y‖) ^ 2 := by
    exact (sq_le_sq₀ (norm_nonneg _) hnonneg).2 hnorm
  have hjensen : (a * ‖x‖ + b * ‖y‖) ^ 2 ≤ a * ‖x‖ ^ 2 + b * ‖y‖ ^ 2 := by
    have hdiff_nonneg : 0 ≤ a * b * (‖x‖ - ‖y‖) ^ 2 := by
      exact mul_nonneg (mul_nonneg ha hb) (sq_nonneg _)
    have hident :
        a * ‖x‖ ^ 2 + b * ‖y‖ ^ 2 - (a * ‖x‖ + b * ‖y‖) ^ 2 =
          a * b * (‖x‖ - ‖y‖) ^ 2 := by
      nlinarith [hab]
    nlinarith
  exact hsq.trans hjensen

/-- Nonnegative quadratic norm potentials are convex. -/

Exact module and namespace context

Scope and omitted-condition boundaries

No strict or strong convexity is concluded. A general norm need not arise from an inner product.
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)

convex_univ
norm_add_le
norm_smul
Real.norm_of_nonneg
norm_nonneg
add_nonneg
mul_nonneg
sq_le_sq₀
sq_nonneg

Mathematical sources

Existing ASTIS declaration and exact proof — Directly read current local source; no Lean edit or fresh build.
Existing curated module card — Local API/source-boundary memory; not independent primary textbook verification.
norm_smul — Exact inspected Mathlib definition or theorem used by this exposition.
Real.norm_of_nonneg — Exact inspected Mathlib definition or theorem used by this exposition.
sq_le_sq₀ — Exact inspected Mathlib definition or theorem used by this exposition.
Existing usage in Tests.Basic — Read-only source example; no test was run.
convex_univ — Exact local Mathlib declaration anchor.

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

ASTIS mathematical exposition

Convexity of a quadratic-norm potential

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

Statement

On a real normed vector space E, let a,b∈ℝ with a≥0. Then V=a‖x‖²+b is convex on the entire space. There is no sign restriction on b.

\[V=a\|x\|^2+b,\qquad\operatorname{Convex}_{E}(V)\quad(a\ge0).\]

All objects and hypotheses

E : Type* with [NormedAddCommGroup E] and [NormedSpace ℝ E]. No finite-dimensionality, completeness or inner-product structure is required.
a,b : ℝ; ha : 0≤a; b is 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. Start with the convex base function

The existing squared-norm theorem gives convexity of U(x)=‖x‖² on the whole space.

\[U(\lambda x+\theta y)\le\lambda U(x)+\theta U(y).\]

Corresponding Lean step

convexOn_univ_norm_sq (E := E)

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

2. Multiply by a nonnegative coefficient

Since a≥0, multiplying the convexity inequality by a preserves its direction. This proves convexity of aU.

\[aU(\lambda x+\theta y)\le\lambda aU(x)+\theta aU(y).\]

Corresponding Lean step

have h := (convexOn_univ_norm_sq (E := E)).smul ha

The .smul API scales an inequality; its nonnegative scalar hypothesis is what preserves the inequality direction.

3. Add the constant offset

Add b to both sides and use λ+θ=1 to distribute b as λb+θb. The result is the convexity inequality for V=aU+b.

\[aU(\lambda x+\theta y)+b\le\lambda(aU(x)+b)+\theta(aU(y)+b).\]

Corresponding Lean step

simpa only [smul_eq_mul] using h.add_const b

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 · convexOn_univ_const_mul_norm_sq_add

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. This declaration proves a convexity property of a real-valued potential. Its nonnegative scaling and constant addition is the exact transformation used in the source, rather than a Hessian argument requiring extra smoothness.

theorem convexOn_univ_const_mul_norm_sq_add
    {E : Type*} [NormedAddCommGroup E] [NormedSpace ℝ E]
    {a b : ℝ} (ha : 0 ≤ a) :
    ConvexOn ℝ (Set.univ : Set E) (fun x : E => a * ‖x‖ ^ 2 + b)

Exact module and namespace context

Lean proof · convexOn_univ_const_mul_norm_sq_add

theorem convexOn_univ_const_mul_norm_sq_add
    {E : Type*} [NormedAddCommGroup E] [NormedSpace ℝ E]
    {a b : ℝ} (ha : 0 ≤ a) :
    ConvexOn ℝ (Set.univ : Set E) (fun x : E => a * ‖x‖ ^ 2 + b) := by
  have h := (convexOn_univ_norm_sq (E := E)).smul ha
  change ConvexOn ℝ Set.univ ((fun x : E => a * ‖x‖ ^ 2) + fun _ => b)
  simpa only [smul_eq_mul] using h.add_const b

/-- The Gibbs shape of a nonnegative quadratic norm potential is log-concave. -/

Exact module and namespace context

Scope and omitted-condition boundaries

Only convexity is established. Coefficient a=0 is allowed; strong convexity, coercivity and integrability do not follow from this result.
This documentation adds no Lean theorem, compilation evidence, source-equivalence verdict, or new source-fidelity certification.

Source and reuse

ASTIS parents called

AutoSamplingTheory.TechnicalLemmas.Geometry.LogConcavity.convexOn_univ_norm_sq

Mathlib API called (external library)

ConvexOn.smul
ConvexOn.add_const
smul_eq_mul

Mathematical sources

Existing ASTIS declaration and exact proof — Directly read current local source; no Lean edit or fresh build.
Existing curated module card — Local API/source-boundary memory; not independent primary textbook verification.
ConvexOn.smul — Exact inspected Mathlib definition or theorem used by this exposition.
ConvexOn.add_const — Exact inspected Mathlib definition or theorem used by this exposition.
Existing usage in Tests.Basic — Read-only source example; no test was run.

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

ASTIS mathematical exposition

Log-concavity of a quadratic-norm Gibbs shape

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

Statement

On a real normed vector space E, let a,b∈ℝ with a≥0. For the potential V=a‖x‖²+b, the function exp(−V) is strictly positive and log-concave on the whole space.

\[V=a\|x\|^2+b,\qquad\operatorname{LC}_{E}(e^{-V})\quad(a\ge0).\]

All objects and hypotheses

E : Type* with [NormedAddCommGroup E] and [NormedSpace ℝ E]. No finite-dimensionality, completeness or inner-product structure is required.
a,b : ℝ; ha : 0≤a; no sign condition on b.

{'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. Supply the already-proved convex potential

The corresponding potential theorem establishes convexity of V with exactly the supplied a≥0 and the same unrestricted b.

\[\operatorname{Convex}_{E}(V).\]

Corresponding Lean step

convexOn_univ_const_mul_norm_sq_add (E := E) (a := a) (b := b) ha

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

2. Use exponential positivity and the log identity

The generic convex-potential theorem says exp(−V)>0 and log(exp(−V))=−V. Negating the convex potential gives a concave logarithm, so the theorem applies directly.

\[e^{-V}>0,\qquad\log(e^{-V})=-V\text{ is concave}.\]

Corresponding Lean step

simpa using logConcaveOn_exp_neg_of_convexOn
  (convexOn_univ_const_mul_norm_sq_add (E := E) (a := a) (b := b) ha)

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_exp_neg_quadratic_norm

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. simpa only aligns the specialized formula with the generic Gibbs-shape theorem. The argument is reuse of the convex-potential result, not a new integration or differential calculation.

theorem logConcaveOn_exp_neg_quadratic_norm
    {E : Type*} [NormedAddCommGroup E] [NormedSpace ℝ E]
    {a b : ℝ} (ha : 0 ≤ a) :
    LogConcaveOn (Set.univ : Set E) (fun x : E => Real.exp (-(a * ‖x‖ ^ 2 + b)))

Exact module and namespace context

Lean proof · logConcaveOn_exp_neg_quadratic_norm

simpa only aligns the specialized formula with the generic Gibbs-shape theorem. The argument is reuse of the convex-potential result, not a new integration or differential calculation.

theorem logConcaveOn_exp_neg_quadratic_norm
    {E : Type*} [NormedAddCommGroup E] [NormedSpace ℝ E]
    {a b : ℝ} (ha : 0 ≤ a) :
    LogConcaveOn (Set.univ : Set E) (fun x : E => Real.exp (-(a * ‖x‖ ^ 2 + b))) := by
  simpa using logConcaveOn_exp_neg_of_convexOn
    (convexOn_univ_const_mul_norm_sq_add (E := E) (a := a) (b := b) ha)

/-- Positive multiples of nonnegative quadratic Gibbs shapes are log-concave. -/

Exact module and namespace context

Scope and omitted-condition boundaries

The conclusion is log-concavity of a function shape. No normalizing integral, probability law or executable kernel is constructed.
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)

No direct Mathlib call recorded; see the ASTIS parents.

Mathematical sources

Existing ASTIS declaration and exact proof — Directly read current local source; no Lean edit or fresh build.
Existing curated module card — Local API/source-boundary memory; not independent primary textbook verification.
Existing usage in Tests.Basic — Read-only source example; no test was run.

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

ASTIS mathematical exposition

Positive rescaling of the quadratic-norm Gibbs shape

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

Statement

On a real normed vector space E, let a,b,c∈ℝ with a≥0 and c>0. With V=a‖x‖²+b, the function c exp(−V) is positive log-concave on the whole domain. The constant c is not required or proved to normalize an integral.

\[V=a\|x\|^2+b,\qquad a\ge0,\ c>0\Longrightarrow\operatorname{LC}_{E}(ce^{-V}).\]

All objects and hypotheses

E : Type* with [NormedAddCommGroup E] and [NormedSpace ℝ E]. No finite-dimensionality, completeness or inner-product structure is required.
a,b : ℝ; ha : 0≤a; no sign condition on b.
c : ℝ; hc : 0<c.

{'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. Verify the potential's convexity

Reuse the corresponding convexity theorem for V; it requires a≥0 and imposes no bound on b.

\[\operatorname{Convex}_{E}(V).\]

Corresponding Lean step

convexOn_univ_const_mul_norm_sq_add (E := E) (a := a) (b := b) ha

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

2. Apply the positive-rescaled Gibbs-shape theorem

For any positive c, log(c exp(−V))=log c−V is concave and the function itself is positive. Apply the generic result to the verified V and the supplied c>0.

\[\log(ce^{-V})=\log c-V,\qquad ce^{-V}>0.\]

Corresponding Lean step

simpa using logConcaveOn_const_mul_exp_neg_of_convexOn
  (convexOn_univ_const_mul_norm_sq_add (E := E) (a := a) (b := b) ha) hc

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_const_mul_exp_neg_quadratic_norm

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. There are two sign assumptions with different roles: ha lets the potential be convex, and hc keeps the rescaled function strictly positive. The theorem accepts any such c.

theorem logConcaveOn_const_mul_exp_neg_quadratic_norm
    {E : Type*} [NormedAddCommGroup E] [NormedSpace ℝ E]
    {a b c : ℝ} (ha : 0 ≤ a) (hc : 0 < c) :
    LogConcaveOn (Set.univ : Set E)
      (fun x : E => c * Real.exp (-(a * ‖x‖ ^ 2 + b)))

Exact module and namespace context

Lean proof · logConcaveOn_const_mul_exp_neg_quadratic_norm

There are two sign assumptions with different roles: ha lets the potential be convex, and hc keeps the rescaled function strictly positive. The theorem accepts any such c.

theorem logConcaveOn_const_mul_exp_neg_quadratic_norm
    {E : Type*} [NormedAddCommGroup E] [NormedSpace ℝ E]
    {a b c : ℝ} (ha : 0 ≤ a) (hc : 0 < c) :
    LogConcaveOn (Set.univ : Set E)
      (fun x : E => c * Real.exp (-(a * ‖x‖ ^ 2 + b))) := by
  simpa using logConcaveOn_const_mul_exp_neg_of_convexOn
    (convexOn_univ_const_mul_norm_sq_add (E := E) (a := a) (b := b) ha) hc

/-- The explicitly normalized finite-dimensional quadratic Gibbs density is log-concave. -/

Exact module and namespace context

Scope and omitted-condition boundaries

Positive rescaling does not certify a partition function or total mass one.
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)

No direct Mathlib call recorded; see the ASTIS parents.

Mathematical sources

Existing ASTIS declaration and exact proof — Directly read current local source; no Lean edit or fresh build.
Existing curated module card — Local API/source-boundary memory; not independent primary textbook verification.

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

ASTIS mathematical exposition

Log-concavity with the explicit quadratic prefactor

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

Statement

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

\[d=\dim_{\mathbb R}E,\qquad Z=e^{-b}\left(\frac\pi a\right)^{d/2},\qquad V=a\|x\|^2+b,\qquad a>0\Longrightarrow\operatorname{LC}_{E}(Z^{-1}e^{-V}).\]

All objects and hypotheses

E : Type* with [NormedAddCommGroup E] [NormedSpace ℝ E] [FiniteDimensional ℝ E]. There is no inner-product, measurable-space or measure parameter.
a,b : ℝ; ha : 0<a, with b arbitrary.
d denotes Module.finrank ℝ E, cast to ℝ in the real exponent d/2. No inner-product structure, measure or volume normalization is a parameter.

{'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

Let d=finrankℝ(E). Since π>0 and a>0, π/a>0. A real power of a positive base is positive, including d=0. Multiplying by e⁻ᵇ>0 proves positivity of Z; no Gaussian integral is used.

\[\frac\pi a>0,\quad\left(\frac\pi a\right)^{d/2}>0,\quad Z=e^{-b}\left(\frac\pi a\right)^{d/2}>0.\]

Corresponding Lean step

have hZpos : 0 < Real.exp (-b) * (Real.pi / a) ^ ((Module.finrank ℝ E : ℝ) / 2) := by
  exact mul_pos (Real.exp_pos _) (Real.rpow_pos_of_pos (div_pos Real.pi_pos ha) _)

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

\[\operatorname{LC}_{E}(ce^{-V}),\quad c=Z^{-1}\Longrightarrow\operatorname{LC}_{E}(Z^{-1}e^{-V}).\]

Corresponding Lean step

exact logConcaveOn_const_mul_exp_neg_quadratic_norm (E := E) (a := a) (b := b)
  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_quadratic_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.

theorem logConcaveOn_explicit_quadratic_normalized_density
    {E : Type*} [NormedAddCommGroup E] [NormedSpace ℝ E] [FiniteDimensional ℝ E]
    {a b : ℝ} (ha : 0 < a) :
    LogConcaveOn (Set.univ : Set E)
      (fun x : E =>
        (Real.exp (-b) * (Real.pi / a) ^ ((Module.finrank ℝ E : ℝ) / 2))⁻¹ *
          Real.exp (-(a * ‖x‖ ^ 2 + b)))

Exact module and namespace context

Lean proof · logConcaveOn_explicit_quadratic_normalized_density

theorem logConcaveOn_explicit_quadratic_normalized_density
    {E : Type*} [NormedAddCommGroup E] [NormedSpace ℝ E] [FiniteDimensional ℝ E]
    {a b : ℝ} (ha : 0 < a) :
    LogConcaveOn (Set.univ : Set E)
      (fun x : E =>
        (Real.exp (-b) * (Real.pi / a) ^ ((Module.finrank ℝ E : ℝ) / 2))⁻¹ *
          Real.exp (-(a * ‖x‖ ^ 2 + b))) := by
  have hZpos : 0 < Real.exp (-b) * (Real.pi / a) ^ ((Module.finrank ℝ E : ℝ) / 2) := by
    exact mul_pos (Real.exp_pos _) (Real.rpow_pos_of_pos (div_pos Real.pi_pos ha) _)
  exact logConcaveOn_const_mul_exp_neg_quadratic_norm (E := E) (a := a) (b := b)
    ha.le (inv_pos.mpr hZpos)

/-- Shifted nonnegative quadratic norm potentials are convex. -/

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 norm is arbitrary; it is not assumed to be Euclidean. The expression e⁻ᵇ(π/a)^(d/2) is therefore not certified here as a partition function for that norm or for any chosen measure.
This documentation adds no Lean theorem, compilation evidence, source-equivalence verdict, or new source-fidelity certification.

Source and reuse

ASTIS parents called

AutoSamplingTheory.TechnicalLemmas.Geometry.LogConcavity.logConcaveOn_const_mul_exp_neg_quadratic_norm

Mathlib API called (external library)

mul_pos
Real.exp_pos
Real.rpow_pos_of_pos
div_pos
Real.pi_pos
inv_pos
Module.finrank

Mathematical sources

Existing ASTIS declaration and exact proof — Directly read current local source; no Lean edit or fresh build.
Existing curated module card — Local API/source-boundary memory; not independent primary textbook verification.
Real.rpow_pos_of_pos — Exact inspected Mathlib definition or theorem used by this exposition.
Real.pi_pos — Exact inspected Mathlib definition or theorem used by this exposition.
Module.finrank — Exact inspected Mathlib definition or theorem used by this exposition.
Existing usage in Tests.Basic — Read-only source example; no test was run.
Real.exp_pos — Exact local Mathlib declaration anchor.

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

ASTIS mathematical exposition

Convexity of a shifted quadratic-norm potential

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

Statement

On a real normed vector space E, let a,b∈ℝ with a≥0 and fix m∈E. Then V=a‖x-m‖²+b is convex on the entire space. There is no sign restriction on b.

\[V=a\|x-m\|^2+b,\qquad\operatorname{Convex}_{E}(V)\quad(a\ge0).\]

All objects and hypotheses

E : Type* with [NormedAddCommGroup E] and [NormedSpace ℝ E]. No finite-dimensionality, completeness or inner-product structure is required.
a,b : ℝ; ha : 0≤a; b is arbitrary.
m : E is an arbitrary fixed center.

{'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. Construct the translation as an affine map

The map T(x)=x−m has identity linear part: T(p+v)=T(p)+v. The source supplies this equation when building the affine-map structure.

\[T(x)=x-m,\qquad T(p+v)=T(p)+v.\]

Corresponding Lean step

let shift : E →ᵃ[ℝ] E :=
  { toFun := fun x => x - m
    linear := LinearMap.id
    map_vadd' := by intro p v; simp [sub_eq_add_neg, add_assoc] }

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 centered convex potential

The centered function U(z)=a‖z‖²+b is convex on E by the existing nonnegative-quadratic-potential theorem.

\[U(z)=a\|z\|^2+b,\qquad U\text{ convex on }E.\]

Corresponding Lean step

convexOn_univ_const_mul_norm_sq_add (E := E) (a := a) (b := b) ha

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

3. Precompose with the affine translation

Affine maps preserve convex combinations, so convexity transfers from U to U∘T. The inverse image of the whole space is the whole space, and U(T(x)) is the desired shifted potential.

\[U(T(\lambda x+\theta y))=U(\lambda T(x)+\theta T(y))\le\lambda U(T(x))+\theta U(T(y)).\]

Corresponding Lean step

have h := (convexOn_univ_const_mul_norm_sq_add (E := E) (a := a) (b := b) ha).comp_affineMap shift
change ConvexOn ℝ Set.univ ((fun x : E => a * ‖x‖ ^ 2 + b) ∘ shift)
exact h

The affine-map API uses preservation of convex combinations, including that the coefficients sum to one.

Lean statement · convexOn_univ_const_mul_norm_sub_sq_add

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. This declaration proves a convexity property of a real-valued potential. Its translation is the exact transformation used in the source, rather than a Hessian argument requiring extra smoothness.

theorem convexOn_univ_const_mul_norm_sub_sq_add
    {E : Type*} [NormedAddCommGroup E] [NormedSpace ℝ E]
    {a b : ℝ} (m : E) (ha : 0 ≤ a) :
    ConvexOn ℝ (Set.univ : Set E) (fun x : E => a * ‖x - m‖ ^ 2 + b)

Exact module and namespace context

Lean proof · convexOn_univ_const_mul_norm_sub_sq_add

This declaration proves a convexity property of a real-valued potential. Its translation is the exact transformation used in the source, rather than a Hessian argument requiring extra smoothness.

theorem convexOn_univ_const_mul_norm_sub_sq_add
    {E : Type*} [NormedAddCommGroup E] [NormedSpace ℝ E]
    {a b : ℝ} (m : E) (ha : 0 ≤ a) :
    ConvexOn ℝ (Set.univ : Set E) (fun x : E => a * ‖x - m‖ ^ 2 + b) := by
  let shift : E →ᵃ[ℝ] E :=
    { toFun := fun x => x - m
      linear := LinearMap.id
      map_vadd' := by
        intro p v
        simp [sub_eq_add_neg, add_assoc] }
  have h :=
    (convexOn_univ_const_mul_norm_sq_add (E := E) (a := a) (b := b) ha).comp_affineMap
      shift
  change ConvexOn ℝ Set.univ
    ((fun x : E => a * ‖x‖ ^ 2 + b) ∘ shift)
  exact h

/-- The Gibbs shape of a shifted nonnegative quadratic norm potential is log-concave. -/

Exact module and namespace context

Scope and omitted-condition boundaries

Only convexity is established. Coefficient a=0 is allowed; strong convexity, coercivity and integrability do not follow from this result.
This documentation adds no Lean theorem, compilation evidence, source-equivalence verdict, or new source-fidelity certification.

Source and reuse

ASTIS parents called

AutoSamplingTheory.TechnicalLemmas.Geometry.LogConcavity.convexOn_univ_const_mul_norm_sq_add

Mathlib API called (external library)

LinearMap.id
ConvexOn.comp_affineMap
sub_eq_add_neg
add_assoc

Mathematical sources

Existing ASTIS declaration and exact proof — Directly read current local source; no Lean edit or fresh build.
Existing curated module card — Local API/source-boundary memory; not independent primary textbook verification.
ConvexOn.comp_affineMap — Exact inspected Mathlib definition or theorem used by this exposition.
Existing usage in Tests.Basic — Read-only source example; no test was run.
LinearMap.id — Exact local Mathlib declaration anchor.

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

ASTIS mathematical exposition

Log-concavity of a shifted quadratic-norm Gibbs shape

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

Statement

On a real normed vector space E, let a,b∈ℝ with a≥0 and m∈E fixed. For the potential V=a‖x-m‖²+b, the function exp(−V) is strictly positive and log-concave on the whole space.

\[V=a\|x-m\|^2+b,\qquad\operatorname{LC}_{E}(e^{-V})\quad(a\ge0).\]

All objects and hypotheses

E : Type* with [NormedAddCommGroup E] and [NormedSpace ℝ E]. No finite-dimensionality, completeness or inner-product structure is required.
a,b : ℝ; ha : 0≤a; no sign condition on b.
m : E is an arbitrary fixed center.

{'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. Supply the already-proved convex potential

The corresponding potential theorem establishes convexity of V with exactly the supplied a≥0 and the same unrestricted b and fixed center m.

\[\operatorname{Convex}_{E}(V).\]

Corresponding Lean step

convexOn_univ_const_mul_norm_sub_sq_add (E := E) (a := a) (b := b) m ha

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

2. Use exponential positivity and the log identity

The generic convex-potential theorem says exp(−V)>0 and log(exp(−V))=−V. Negating the convex potential gives a concave logarithm, so the theorem applies directly.

\[e^{-V}>0,\qquad\log(e^{-V})=-V\text{ is concave}.\]

Corresponding Lean step

simpa using logConcaveOn_exp_neg_of_convexOn
  (convexOn_univ_const_mul_norm_sub_sq_add (E := E) (a := a) (b := b) m ha)

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_exp_neg_shifted_quadratic_norm

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. simpa only aligns the specialized formula with the generic Gibbs-shape theorem. The argument is reuse of the convex-potential result, not a new integration or differential calculation.

theorem logConcaveOn_exp_neg_shifted_quadratic_norm
    {E : Type*} [NormedAddCommGroup E] [NormedSpace ℝ E]
    {a b : ℝ} (m : E) (ha : 0 ≤ a) :
    LogConcaveOn (Set.univ : Set E)
      (fun x : E => Real.exp (-(a * ‖x - m‖ ^ 2 + b)))

Exact module and namespace context

Lean proof · logConcaveOn_exp_neg_shifted_quadratic_norm

simpa only aligns the specialized formula with the generic Gibbs-shape theorem. The argument is reuse of the convex-potential result, not a new integration or differential calculation.

theorem logConcaveOn_exp_neg_shifted_quadratic_norm
    {E : Type*} [NormedAddCommGroup E] [NormedSpace ℝ E]
    {a b : ℝ} (m : E) (ha : 0 ≤ a) :
    LogConcaveOn (Set.univ : Set E)
      (fun x : E => Real.exp (-(a * ‖x - m‖ ^ 2 + b))) := by
  simpa using logConcaveOn_exp_neg_of_convexOn
    (convexOn_univ_const_mul_norm_sub_sq_add (E := E) (a := a) (b := b) m ha)

/-- Positive multiples of shifted nonnegative quadratic Gibbs shapes are log-concave. -/

Exact module and namespace context

Scope and omitted-condition boundaries

The conclusion is log-concavity of a function shape. No normalizing integral, probability law or executable kernel is constructed.
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)

No direct Mathlib call recorded; see the ASTIS parents.

Mathematical sources

Existing ASTIS declaration and exact proof — Directly read current local source; no Lean edit or fresh build.
Existing curated module card — Local API/source-boundary memory; not independent primary textbook verification.
Existing usage in Tests.Basic — Read-only source example; no test was run.

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

ASTIS mathematical exposition

Positive rescaling of the shifted quadratic-norm Gibbs shape

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

Statement

On a real normed vector space E, let a,b,c∈ℝ with a≥0 and c>0, and let m∈E be fixed. With V=a‖x-m‖²+b, the function c exp(−V) is positive log-concave on the whole domain. The constant c is not required or proved to normalize an integral.

\[V=a\|x-m\|^2+b,\qquad a\ge0,\ c>0\Longrightarrow\operatorname{LC}_{E}(ce^{-V}).\]

All objects and hypotheses

E : Type* with [NormedAddCommGroup E] and [NormedSpace ℝ E]. No finite-dimensionality, completeness or inner-product structure is required.
a,b : ℝ; ha : 0≤a; no sign condition on b.
m : E is an arbitrary fixed center.
c : ℝ; hc : 0<c.

{'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. Verify the potential's convexity

Reuse the corresponding convexity theorem for V; it requires a≥0 and imposes no bound on b.

\[\operatorname{Convex}_{E}(V).\]

Corresponding Lean step

convexOn_univ_const_mul_norm_sub_sq_add (E := E) (a := a) (b := b) m ha

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

2. Apply the positive-rescaled Gibbs-shape theorem

For any positive c, log(c exp(−V))=log c−V is concave and the function itself is positive. Apply the generic result to the verified V and the supplied c>0.

\[\log(ce^{-V})=\log c-V,\qquad ce^{-V}>0.\]

Corresponding Lean step

simpa using logConcaveOn_const_mul_exp_neg_of_convexOn
  (convexOn_univ_const_mul_norm_sub_sq_add (E := E) (a := a) (b := b) m ha) hc

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_const_mul_exp_neg_shifted_quadratic_norm

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. There are two sign assumptions with different roles: ha lets the potential be convex, and hc keeps the rescaled function strictly positive. The theorem accepts any such c.

theorem logConcaveOn_const_mul_exp_neg_shifted_quadratic_norm
    {E : Type*} [NormedAddCommGroup E] [NormedSpace ℝ E]
    {a b c : ℝ} (m : E) (ha : 0 ≤ a) (hc : 0 < c) :
    LogConcaveOn (Set.univ : Set E)
      (fun x : E => c * Real.exp (-(a * ‖x - m‖ ^ 2 + b)))

Exact module and namespace context

Lean proof · logConcaveOn_const_mul_exp_neg_shifted_quadratic_norm

There are two sign assumptions with different roles: ha lets the potential be convex, and hc keeps the rescaled function strictly positive. The theorem accepts any such c.

theorem logConcaveOn_const_mul_exp_neg_shifted_quadratic_norm
    {E : Type*} [NormedAddCommGroup E] [NormedSpace ℝ E]
    {a b c : ℝ} (m : E) (ha : 0 ≤ a) (hc : 0 < c) :
    LogConcaveOn (Set.univ : Set E)
      (fun x : E => c * Real.exp (-(a * ‖x - m‖ ^ 2 + b))) := by
  simpa using logConcaveOn_const_mul_exp_neg_of_convexOn
    (convexOn_univ_const_mul_norm_sub_sq_add (E := E) (a := a) (b := b) m ha) hc

/-- The explicitly normalized shifted finite-dimensional quadratic Gibbs density is log-concave. -/

Exact module and namespace context

Scope and omitted-condition boundaries

Positive rescaling does not certify a partition function or total mass one.
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)

No direct Mathlib call recorded; see the ASTIS parents.

Mathematical sources

Existing ASTIS declaration and exact proof — Directly read current local source; no Lean edit or fresh build.
Existing curated module card — Local API/source-boundary memory; not independent primary textbook verification.

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

ASTIS mathematical exposition

Log-concavity with the explicit quadratic prefactor after translation

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

Statement

Let E be a finite-dimensional real normed vector space and set d=dimℝE; let a,b∈ℝ with a>0, and fix m∈E. Put V=a‖x-m‖²+b and Z=exp(−b)(π/a)^(d/2). Then the explicitly scaled function Z⁻¹ exp(−V) is positive log-concave on E. The theorem proves only this shape property; despite the existing declaration's name, it supplies no equality between Z and an integral.

\[d=\dim_{\mathbb R}E,\qquad Z=e^{-b}\left(\frac\pi a\right)^{d/2},\qquad V=a\|x-m\|^2+b,\qquad a>0\Longrightarrow\operatorname{LC}_{E}(Z^{-1}e^{-V}).\]

All objects and hypotheses

E : Type* with [NormedAddCommGroup E] [NormedSpace ℝ E] [FiniteDimensional ℝ E]. There is no inner-product, measurable-space or measure parameter.
a,b : ℝ; ha : 0<a, with b arbitrary.
m : E is an arbitrary fixed center.
d denotes Module.finrank ℝ E, cast to ℝ in the real exponent d/2. No inner-product structure, measure or volume normalization is a parameter.

{'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

Let d=finrankℝ(E). Since π>0 and a>0, π/a>0. A real power of a positive base is positive, including d=0. Multiplying by e⁻ᵇ>0 proves positivity of Z; no Gaussian integral is used.

\[\frac\pi a>0,\quad\left(\frac\pi a\right)^{d/2}>0,\quad Z=e^{-b}\left(\frac\pi a\right)^{d/2}>0.\]

Corresponding Lean step

have hZpos : 0 < Real.exp (-b) * (Real.pi / a) ^ ((Module.finrank ℝ E : ℝ) / 2) := by
  exact mul_pos (Real.exp_pos _) (Real.rpow_pos_of_pos (div_pos Real.pi_pos ha) _)

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

\[\operatorname{LC}_{E}(ce^{-V}),\quad c=Z^{-1}\Longrightarrow\operatorname{LC}_{E}(Z^{-1}e^{-V}).\]

Corresponding Lean step

exact logConcaveOn_const_mul_exp_neg_shifted_quadratic_norm (E := E) (a := a) (b := b) m
  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_shifted_quadratic_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.

theorem logConcaveOn_explicit_shifted_quadratic_normalized_density
    {E : Type*} [NormedAddCommGroup E] [NormedSpace ℝ E] [FiniteDimensional ℝ E]
    {a b : ℝ} (m : E) (ha : 0 < a) :
    LogConcaveOn (Set.univ : Set E)
      (fun x : E =>
        (Real.exp (-b) * (Real.pi / a) ^ ((Module.finrank ℝ E : ℝ) / 2))⁻¹ *
          Real.exp (-(a * ‖x - m‖ ^ 2 + b)))

Exact module and namespace context

Lean proof · logConcaveOn_explicit_shifted_quadratic_normalized_density

theorem logConcaveOn_explicit_shifted_quadratic_normalized_density
    {E : Type*} [NormedAddCommGroup E] [NormedSpace ℝ E] [FiniteDimensional ℝ E]
    {a b : ℝ} (m : E) (ha : 0 < a) :
    LogConcaveOn (Set.univ : Set E)
      (fun x : E =>
        (Real.exp (-b) * (Real.pi / a) ^ ((Module.finrank ℝ E : ℝ) / 2))⁻¹ *
          Real.exp (-(a * ‖x - m‖ ^ 2 + b))) := by
  have hZpos : 0 < Real.exp (-b) * (Real.pi / a) ^ ((Module.finrank ℝ E : ℝ) / 2) := by
    exact mul_pos (Real.exp_pos _) (Real.rpow_pos_of_pos (div_pos Real.pi_pos ha) _)
  exact logConcaveOn_const_mul_exp_neg_shifted_quadratic_norm
    (E := E) (a := a) (b := b) m ha.le (inv_pos.mpr hZpos)

/-- The two-point quadratic potential `(x, y) ↦ a‖x-y‖^2+b` is convex. -/

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 norm is arbitrary; it is not assumed to be Euclidean. The expression e⁻ᵇ(π/a)^(d/2) is therefore not certified here as a partition function for that norm or for any chosen measure.
This documentation adds no Lean theorem, compilation evidence, source-equivalence verdict, or new source-fidelity certification.

Source and reuse

ASTIS parents called

AutoSamplingTheory.TechnicalLemmas.Geometry.LogConcavity.logConcaveOn_const_mul_exp_neg_shifted_quadratic_norm

Mathlib API called (external library)

mul_pos
Real.exp_pos
Real.rpow_pos_of_pos
div_pos
Real.pi_pos
inv_pos
Module.finrank

Mathematical sources

Existing ASTIS declaration and exact proof — Directly read current local source; no Lean edit or fresh build.
Existing curated module card — Local API/source-boundary memory; not independent primary textbook verification.
Real.rpow_pos_of_pos — Exact inspected Mathlib definition or theorem used by this exposition.
Real.pi_pos — Exact inspected Mathlib definition or theorem used by this exposition.
Module.finrank — Exact inspected Mathlib definition or theorem used by this exposition.
Existing usage in Tests.Basic — Read-only source example; no test was run.
Real.exp_pos — Exact local Mathlib declaration anchor.

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

ASTIS mathematical exposition

Convexity of a two-point difference-quadratic potential

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

Statement

On the Cartesian product E×E of a real normed vector space E with itself, let a,b∈ℝ with a≥0. Then V=a‖x-y‖²+b is convex on the entire product space. There is no sign restriction on b.

\[V=a\|x-y\|^2+b,\qquad\operatorname{Convex}_{E\times E}(V)\quad(a\ge0).\]

All objects and hypotheses

E : Type* with [NormedAddCommGroup E] and [NormedSpace ℝ E]. No finite-dimensionality, completeness or inner-product structure is required.
a,b : ℝ; ha : 0≤a; b is 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. Construct the linear difference map

Subtract the two coordinate-projection linear maps. The result D(x,y)=x−y is linear and therefore preserves every weighted sum.

\[D(x,y)=x-y,\qquad D(\lambda u+\theta v)=\lambda D(u)+\theta D(v).\]

Corresponding Lean step

let diff : E × E →ₗ[ℝ] E := LinearMap.fst ℝ E E - LinearMap.snd ℝ E E

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 convexity of the centered potential

U(z)=a‖z‖²+b is convex on E under a≥0.

\[U(z)=a\|z\|^2+b,\qquad U\text{ convex on }E.\]

Corresponding Lean step

convexOn_univ_const_mul_norm_sq_add (E := E) (a := a) (b := b) ha

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

3. Pull convexity back along D

Apply the linear-precomposition theorem to U and D. Its domain is all E×E and U(D(x,y))=a‖x−y‖²+b.

\[(U\circ D)(\lambda u+\theta v)\le\lambda(U\circ D)(u)+\theta(U\circ D)(v).\]

Corresponding Lean step

have h := (convexOn_univ_const_mul_norm_sq_add (E := E) (a := a) (b := b) ha).comp_linearMap diff
change ConvexOn ℝ Set.univ ((fun x : E => a * ‖x‖ ^ 2 + b) ∘ diff)
exact h

The linear-map API pulls back the domain and applies the existing inequality to mapped endpoints.

Lean statement · convexOn_univ_const_mul_norm_fst_sub_snd_sq_add

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. This declaration proves a convexity property of a real-valued potential. Its difference map is the exact transformation used in the source, rather than a Hessian argument requiring extra smoothness.

theorem convexOn_univ_const_mul_norm_fst_sub_snd_sq_add
    {E : Type*} [NormedAddCommGroup E] [NormedSpace ℝ E]
    {a b : ℝ} (ha : 0 ≤ a) :
    ConvexOn ℝ (Set.univ : Set (E × E))
      (fun z : E × E => a * ‖z.1 - z.2‖ ^ 2 + b)

Exact module and namespace context

Lean proof · convexOn_univ_const_mul_norm_fst_sub_snd_sq_add

This declaration proves a convexity property of a real-valued potential. Its difference map is the exact transformation used in the source, rather than a Hessian argument requiring extra smoothness.

theorem convexOn_univ_const_mul_norm_fst_sub_snd_sq_add
    {E : Type*} [NormedAddCommGroup E] [NormedSpace ℝ E]
    {a b : ℝ} (ha : 0 ≤ a) :
    ConvexOn ℝ (Set.univ : Set (E × E))
      (fun z : E × E => a * ‖z.1 - z.2‖ ^ 2 + b) := by
  let diff : E × E →ₗ[ℝ] E := LinearMap.fst ℝ E E - LinearMap.snd ℝ E E
  have h :=
    (convexOn_univ_const_mul_norm_sq_add (E := E) (a := a) (b := b) ha).comp_linearMap
      diff
  change ConvexOn ℝ Set.univ
    ((fun x : E => a * ‖x‖ ^ 2 + b) ∘ diff)
  exact h

/-- The two-point quadratic Gibbs kernel shape `(x, y) ↦ exp (-(a‖x-y‖^2+b))`
is log-concave on the product space. -/

Exact module and namespace context

Scope and omitted-condition boundaries

Only convexity is established. Coefficient a=0 is allowed; strong convexity, coercivity and integrability do not follow from this result.
This documentation adds no Lean theorem, compilation evidence, source-equivalence verdict, or new source-fidelity certification.

Source and reuse

ASTIS parents called

AutoSamplingTheory.TechnicalLemmas.Geometry.LogConcavity.convexOn_univ_const_mul_norm_sq_add

Mathlib API called (external library)

LinearMap.fst
LinearMap.snd
ConvexOn.comp_linearMap

Mathematical sources

Existing ASTIS declaration and exact proof — Directly read current local source; no Lean edit or fresh build.
Existing curated module card — Local API/source-boundary memory; not independent primary textbook verification.
LinearMap.fst — Exact inspected Mathlib definition or theorem used by this exposition.
LinearMap.snd — Exact inspected Mathlib definition or theorem used by this exposition.
ConvexOn.comp_linearMap — Exact inspected Mathlib definition or theorem used by this exposition.
Existing usage in Tests.Basic — Read-only source example; no test was run.

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

ASTIS mathematical exposition

Log-concavity of a two-point difference-quadratic Gibbs shape

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

Statement

On the Cartesian product E×E of a real normed vector space E with itself, let a,b∈ℝ with a≥0. For the potential V=a‖x-y‖²+b, the function exp(−V) is strictly positive and log-concave on the whole product space.

\[V=a\|x-y\|^2+b,\qquad\operatorname{LC}_{E\times E}(e^{-V})\quad(a\ge0).\]

All objects and hypotheses

E : Type* with [NormedAddCommGroup E] and [NormedSpace ℝ E]. No finite-dimensionality, completeness or inner-product structure is required.
a,b : ℝ; ha : 0≤a; no sign condition on b.

{'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. Supply the already-proved convex potential

The corresponding potential theorem establishes convexity of V with exactly the supplied a≥0 and the same unrestricted b.

\[\operatorname{Convex}_{E\times E}(V).\]

Corresponding Lean step

convexOn_univ_const_mul_norm_fst_sub_snd_sq_add (E := E) (a := a) (b := b) ha

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

2. Use exponential positivity and the log identity

The generic convex-potential theorem says exp(−V)>0 and log(exp(−V))=−V. Negating the convex potential gives a concave logarithm, so the theorem applies directly.

\[e^{-V}>0,\qquad\log(e^{-V})=-V\text{ is concave}.\]

Corresponding Lean step

simpa using logConcaveOn_exp_neg_of_convexOn
  (convexOn_univ_const_mul_norm_fst_sub_snd_sq_add (E := E) (a := a) (b := b) ha)

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_exp_neg_pair_sub_quadratic_norm

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. simpa only aligns the specialized formula with the generic Gibbs-shape theorem. The argument is reuse of the convex-potential result, not a new integration or differential calculation.

theorem logConcaveOn_exp_neg_pair_sub_quadratic_norm
    {E : Type*} [NormedAddCommGroup E] [NormedSpace ℝ E]
    {a b : ℝ} (ha : 0 ≤ a) :
    LogConcaveOn (Set.univ : Set (E × E))
      (fun z : E × E => Real.exp (-(a * ‖z.1 - z.2‖ ^ 2 + b)))

Exact module and namespace context

Lean proof · logConcaveOn_exp_neg_pair_sub_quadratic_norm

simpa only aligns the specialized formula with the generic Gibbs-shape theorem. The argument is reuse of the convex-potential result, not a new integration or differential calculation.

theorem logConcaveOn_exp_neg_pair_sub_quadratic_norm
    {E : Type*} [NormedAddCommGroup E] [NormedSpace ℝ E]
    {a b : ℝ} (ha : 0 ≤ a) :
    LogConcaveOn (Set.univ : Set (E × E))
      (fun z : E × E => Real.exp (-(a * ‖z.1 - z.2‖ ^ 2 + b))) := by
  simpa using logConcaveOn_exp_neg_of_convexOn
    (convexOn_univ_const_mul_norm_fst_sub_snd_sq_add (E := E) (a := a) (b := b) ha)

/-- Positive multiples of two-point quadratic Gibbs kernel shapes are log-concave. -/

Exact module and namespace context

Scope and omitted-condition boundaries

The conclusion is log-concavity of a function shape. No normalizing integral, probability law or executable kernel is constructed.
The word kernel in surrounding names refers to a two-point function, not a ProbabilityTheory.Kernel or a Markov property.
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)

No direct Mathlib call recorded; see the ASTIS parents.

Mathematical sources

Existing ASTIS declaration and exact proof — Directly read current local source; no Lean edit or fresh build.
Existing curated module card — Local API/source-boundary memory; not independent primary textbook verification.
Existing usage in Tests.Basic — Read-only source example; no test was run.

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

ASTIS mathematical exposition

Positive rescaling of the two-point difference-quadratic Gibbs shape

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

Statement

On the Cartesian product E×E of a real normed vector space E with itself, let a,b,c∈ℝ with a≥0 and c>0. With V=a‖x-y‖²+b, the function c exp(−V) is positive log-concave on the whole domain. The constant c is not required or proved to normalize an integral.

\[V=a\|x-y\|^2+b,\qquad a\ge0,\ c>0\Longrightarrow\operatorname{LC}_{E\times E}(ce^{-V}).\]

All objects and hypotheses

E : Type* with [NormedAddCommGroup E] and [NormedSpace ℝ E]. No finite-dimensionality, completeness or inner-product structure is required.
a,b : ℝ; ha : 0≤a; no sign condition on b.
c : ℝ; hc : 0<c.

{'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. Verify the potential's convexity

Reuse the corresponding convexity theorem for V; it requires a≥0 and imposes no bound on b.

\[\operatorname{Convex}_{E\times E}(V).\]

Corresponding Lean step

convexOn_univ_const_mul_norm_fst_sub_snd_sq_add (E := E) (a := a) (b := b) ha

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

2. Apply the positive-rescaled Gibbs-shape theorem

For any positive c, log(c exp(−V))=log c−V is concave and the function itself is positive. Apply the generic result to the verified V and the supplied c>0.

\[\log(ce^{-V})=\log c-V,\qquad ce^{-V}>0.\]

Corresponding Lean step

simpa using logConcaveOn_const_mul_exp_neg_of_convexOn
  (convexOn_univ_const_mul_norm_fst_sub_snd_sq_add (E := E) (a := a) (b := b) ha) hc

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_const_mul_exp_neg_pair_sub_quadratic_norm

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. There are two sign assumptions with different roles: ha lets the potential be convex, and hc keeps the rescaled function strictly positive. The theorem accepts any such c.

theorem logConcaveOn_const_mul_exp_neg_pair_sub_quadratic_norm
    {E : Type*} [NormedAddCommGroup E] [NormedSpace ℝ E]
    {a b c : ℝ} (ha : 0 ≤ a) (hc : 0 < c) :
    LogConcaveOn (Set.univ : Set (E × E))
      (fun z : E × E => c * Real.exp (-(a * ‖z.1 - z.2‖ ^ 2 + b)))

Exact module and namespace context

Lean proof · logConcaveOn_const_mul_exp_neg_pair_sub_quadratic_norm

There are two sign assumptions with different roles: ha lets the potential be convex, and hc keeps the rescaled function strictly positive. The theorem accepts any such c.

theorem logConcaveOn_const_mul_exp_neg_pair_sub_quadratic_norm
    {E : Type*} [NormedAddCommGroup E] [NormedSpace ℝ E]
    {a b c : ℝ} (ha : 0 ≤ a) (hc : 0 < c) :
    LogConcaveOn (Set.univ : Set (E × E))
      (fun z : E × E => c * Real.exp (-(a * ‖z.1 - z.2‖ ^ 2 + b))) := by
  simpa using logConcaveOn_const_mul_exp_neg_of_convexOn
    (convexOn_univ_const_mul_norm_fst_sub_snd_sq_add (E := E) (a := a) (b := b) ha) hc

/-- The finite-dimensional Gaussian-kernel normalizing constant times
`exp (-(a‖x-y‖^2+b))` is log-concave as a function of `(x, y)`.

This is a geometry/kernel-shape leaf.  It does not claim that the function is a
probability density on the full product space. -/

Exact module and namespace context

Scope and omitted-condition boundaries

Positive rescaling does not certify a partition function or total mass one.
Joint log-concavity on E×E is not a probability density or Markov transition assertion.
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)

No direct Mathlib call recorded; see the ASTIS parents.

Mathematical sources

Existing ASTIS declaration and exact proof — Directly read current local source; no Lean edit or fresh build.
Existing curated module card — Local API/source-boundary memory; not independent primary textbook verification.

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

ASTIS mathematical exposition

Log-concavity with the explicit quadratic prefactor on the pair space

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

Statement

Let E be a finite-dimensional real normed vector space and set d=dimℝE; let a,b∈ℝ with a>0. Put V=a‖x-y‖²+b and Z=exp(−b)(π/a)^(d/2). Then the explicitly scaled function Z⁻¹ exp(−V) is positive log-concave on E×E. The theorem proves only this shape property; despite the existing declaration's name, it supplies no equality between Z and an integral.

\[d=\dim_{\mathbb R}E,\qquad Z=e^{-b}\left(\frac\pi a\right)^{d/2},\qquad V=a\|x-y\|^2+b,\qquad a>0\Longrightarrow\operatorname{LC}_{E\times E}(Z^{-1}e^{-V}).\]

All objects and hypotheses

E : Type* with [NormedAddCommGroup E] [NormedSpace ℝ E] [FiniteDimensional ℝ E]. There is no inner-product, measurable-space or measure parameter.
a,b : ℝ; ha : 0<a, with b arbitrary.
d denotes Module.finrank ℝ E, cast to ℝ in the real exponent d/2. No inner-product structure, measure or volume normalization is a parameter.

{'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

Let d=finrankℝ(E). Since π>0 and a>0, π/a>0. A real power of a positive base is positive, including d=0. Multiplying by e⁻ᵇ>0 proves positivity of Z; no Gaussian integral is used.

\[\frac\pi a>0,\quad\left(\frac\pi a\right)^{d/2}>0,\quad Z=e^{-b}\left(\frac\pi a\right)^{d/2}>0.\]

Corresponding Lean step

have hZpos : 0 < Real.exp (-b) * (Real.pi / a) ^ ((Module.finrank ℝ E : ℝ) / 2) := by
  exact mul_pos (Real.exp_pos _) (Real.rpow_pos_of_pos (div_pos Real.pi_pos ha) _)

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

\[\operatorname{LC}_{E\times E}(ce^{-V}),\quad c=Z^{-1}\Longrightarrow\operatorname{LC}_{E\times E}(Z^{-1}e^{-V}).\]

Corresponding Lean step

exact logConcaveOn_const_mul_exp_neg_pair_sub_quadratic_norm (E := E) (a := a) (b := b)
  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_pair_sub_quadratic_kernel

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.

theorem logConcaveOn_explicit_pair_sub_quadratic_kernel
    {E : Type*} [NormedAddCommGroup E] [NormedSpace ℝ E] [FiniteDimensional ℝ E]
    {a b : ℝ} (ha : 0 < a) :
    LogConcaveOn (Set.univ : Set (E × E))
      (fun z : E × E =>
        (Real.exp (-b) * (Real.pi / a) ^ ((Module.finrank ℝ E : ℝ) / 2))⁻¹ *
          Real.exp (-(a * ‖z.1 - z.2‖ ^ 2 + b)))

Exact module and namespace context

Lean proof · logConcaveOn_explicit_pair_sub_quadratic_kernel

theorem logConcaveOn_explicit_pair_sub_quadratic_kernel
    {E : Type*} [NormedAddCommGroup E] [NormedSpace ℝ E] [FiniteDimensional ℝ E]
    {a b : ℝ} (ha : 0 < a) :
    LogConcaveOn (Set.univ : Set (E × E))
      (fun z : E × E =>
        (Real.exp (-b) * (Real.pi / a) ^ ((Module.finrank ℝ E : ℝ) / 2))⁻¹ *
          Real.exp (-(a * ‖z.1 - z.2‖ ^ 2 + b))) := by
  have hZpos : 0 < Real.exp (-b) * (Real.pi / a) ^ ((Module.finrank ℝ E : ℝ) / 2) := by
    exact mul_pos (Real.exp_pos _) (Real.rpow_pos_of_pos (div_pos Real.pi_pos ha) _)
  exact logConcaveOn_const_mul_exp_neg_pair_sub_quadratic_norm
    (E := E) (a := a) (b := b) ha.le (inv_pos.mpr hZpos)

/-- The identity density on the positive ray is log-concave. -/

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 norm is arbitrary; it is not assumed to be Euclidean. The expression e⁻ᵇ(π/a)^(d/2) is therefore not certified here as a partition function for that norm or for any chosen measure.
The domain is the full pair space E×E. The function is not asserted to be a joint probability density there, nor is a Markov kernel constructed.
This documentation adds no Lean theorem, compilation evidence, source-equivalence verdict, or new source-fidelity certification.

Source and reuse

ASTIS parents called

AutoSamplingTheory.TechnicalLemmas.Geometry.LogConcavity.logConcaveOn_const_mul_exp_neg_pair_sub_quadratic_norm

Mathlib API called (external library)

mul_pos
Real.exp_pos
Real.rpow_pos_of_pos
div_pos
Real.pi_pos
inv_pos
Module.finrank

Mathematical sources

Existing ASTIS declaration and exact proof — Directly read current local source; no Lean edit or fresh build.
Existing curated module card — Local API/source-boundary memory; not independent primary textbook verification.
Real.rpow_pos_of_pos — Exact inspected Mathlib definition or theorem used by this exposition.
Real.pi_pos — Exact inspected Mathlib definition or theorem used by this exposition.
Module.finrank — Exact inspected Mathlib definition or theorem used by this exposition.
Existing usage in Tests.Basic — Read-only source example; no test was run.
Real.exp_pos — Exact local Mathlib declaration anchor.

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

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.

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.

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

AutoSamplingTheory.TechnicalLemmas.Geometry.LogConcavity.LogConcaveOn

Mathlib API called (external library)

strictConcaveOn_log_Ioi
StrictConcaveOn.concaveOn

Mathematical sources

Existing ASTIS declaration and exact proof — Directly read current local source; no Lean edit or fresh build.
Existing curated module card — Local API/source-boundary memory; not independent primary textbook verification.
strictConcaveOn_log_Ioi — Exact inspected Mathlib definition or theorem used by this exposition.
StrictConcaveOn.concaveOn — Exact inspected Mathlib definition or theorem used by this exposition.
Existing usage in Tests.Basic — Read-only source example; no test was run.
Existing usage in Tests.Basic — Read-only source example; no test was run.

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