Samplinglib mathematical lesson

Tensor products are log-concave on product domains

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

Read this first

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

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.

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

Proof roadmap

1Check 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.
2Apply 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.
3Rewrite 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.

Full assumptions and notation

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 verification

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

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.

Download module (.lean)

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

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.

Sources, dependencies, and reuse

Source and reuse

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

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