Samplinglib
Lean gate not recorded for this source state main · 9bb7a7394ab0
Samplinglib mathematical lesson

Products on a common domain preserve positive log-concavity

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

Read this first

Mathematical 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).\]
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.

Download module (.lean)
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

Proof roadmap

  1. 1Prove product positivity

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

  2. 2Add the two concave logarithms

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

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

Full assumptions and notation

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 verification

The exact proof begins folded immediately after the mathematical argument; the statement is folded beside the claim above.

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.

Download module (.lean)
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

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.
Sources, dependencies, and reuse

Source and reuse

Samplinglib parents called

Mathlib API called (external library)

  • mul_pos
  • ConcaveOn.add
  • ConcaveOn.congr
  • Real.log_mul

Mathematical sources

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