Samplinglib
Lean gate not recorded for this source state main · 0e31a3cda412
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.

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

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

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