Positive rescaling preserves log-concavity

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

Statement

Let E be a real module, f:E→ℝ positive log-concave on s⊆E, and c>0 a real constant. Then x↦c f(x) is positive log-concave on s.

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 : E → ℝ, hf : LogConcaveOn s f.
• c : ℝ and hc : 0<c.

• {'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

have hconst := concaveOn_const (Real.log c) hf.convex_domain
have hsum := hconst.add hf.concaveOn_log

refine hsum.congr ?_
intro x hx
simpa using (Real.log_mul hc.ne' (hf.pos (x := x) hx).ne').symm

theorem LogConcaveOn.const_mul {E : Type*} [AddCommMonoid E] [Module ℝ E]
    {s : Set E} {f : E → ℝ}
    (hf : LogConcaveOn s f) {c : ℝ} (hc : 0 < c) :
    LogConcaveOn s (fun x => c * f x)

theorem LogConcaveOn.const_mul {E : Type*} [AddCommMonoid E] [Module ℝ E]
    {s : Set E} {f : E → ℝ}
    (hf : LogConcaveOn s f) {c : ℝ} (hc : 0 < c) :
    LogConcaveOn s (fun x => c * f x) := by
  refine ⟨fun x hx => mul_pos hc (hf.pos (x := x) hx), ?_⟩
  have hconst : ConcaveOn ℝ s (fun _ : E => Real.log c) :=
    concaveOn_const (Real.log c) hf.convex_domain
  have hsum :
      ConcaveOn ℝ s ((fun _ : E => Real.log c) + fun x => Real.log (f x)) :=
    hconst.add hf.concaveOn_log
  refine hsum.congr ?_
  intro x hx
  simpa using (Real.log_mul hc.ne' (hf.pos (x := x) hx).ne').symm

/-- A positive constant function is log-concave on every convex domain. -/

Scope and omitted-condition boundaries

• An arbitrary positive rescaling is not automatically a probability normalization.
• This documentation adds no Lean theorem, compilation evidence, source-equivalence verdict, or new source-fidelity certification.