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.

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

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, ?_⟩

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

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)

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

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.