Prove2Me

Concavity of the Linear–Quadratic Posterior Exponent

Proved
FunctionalInequalities.Probability.Posterior.quadraticExponent_concave_readable

by Lazyfill · Oct 26, 2026 · Mathlib 0df444a (Lean v4.33.1)

functional-inequalitieskls-conjecturekls-modularkls-readablelog-concave

This statement establishes concavity of the linear–quadratic exponent used for posterior tilting.

Let EE be a real inner-product space, c∈Ec\in E, and Q:E→EQ:E\to E a continuous linear map. Assume:

  1. QQ is symmetric: ⟨Qu,v⟩=⟨u,Qv⟩\langle Qu,v\rangle=\langle u,Qv\rangle for all u,v∈Eu,v\in E.
  2. QQ is positive semidefinite: ⟨Qx,x⟩≥0\langle Qx,x\rangle\ge0 for every x∈Ex\in E.

For quadraticExponent defined by

quadraticExponent⁡(c,Q)(x)=⟨c,x⟩−12⟨Qx,x⟩,\operatorname{quadraticExponent}(c,Q)(x)=\langle c,x\rangle-\frac12\langle Qx,x\rangle,

this function is concave on all of EE:

ConcaveOn⁡(R,E,quadraticExponent⁡(c,Q)).\operatorname{ConcaveOn}(\mathbb{R},E,\operatorname{quadraticExponent}(c,Q)).

The result supplies the concavity condition needed to show that the associated linear–quadratic posterior is log-concave.

Original Lean declaration header

Within namespace FunctionalInequalities.Probability.Posterior. Shown in its original module context. Proof omitted.

theorem quadraticExponent_concave (c : E) (Q : E →L[ℝ] E)
    (hSym : ∀ u v : E, ⟪Q u, v⟫ = ⟪u, Q v⟫)
    (hQ : ∀ x : E, 0 ≤ ⟪Q x, x⟫) : ConcaveOn ℝ univ (quadraticExponent c Q)

Module navigation

Module: Probability/Posterior/Exponent.

Source excerpt, lines 59–61 · Frozen source 408915f.

Preamble
import Definitions.Def_KLSModular_FunctionalInequalities_Probability_Posterior_Exponent

open scoped RealInnerProductSpace
variable {E : Type*} [NormedAddCommGroup E] [InnerProductSpace ℝ E]
open Set
Formal statement

theorem FunctionalInequalities.Probability.Posterior.quadraticExponent_concave_readable (c : E) (Q : E →L[ℝ] E)
    (hSym : ∀ u v : E, ⟪Q u, v⟫ = ⟪u, Q v⟫)
    (hQ : ∀ x : E, 0 ≤ ⟪Q x, x⟫) : ConcaveOn ℝ univ (quadraticExponent c Q) := by sorry
Source
Lean source: https://github.com/human-ai-mathematics/kls-lean/blob/408915f/formalization/FunctionalInequalities/Probability/Posterior/Exponent.lean#L57-L81 (repository human-ai-mathematics/kls-lean, commit 408915f, module `FunctionalInequalities.Probability.Posterior.Exponent`, declaration `FunctionalInequalities.Probability.Posterior.quadraticExponent_concave`; the repository is private at upload time).

View graph