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

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_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.

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

theorem LogConcaveOn.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

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)) := 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.