1 Balanced Vector Optimization
1.1 Introduction
This blueprint documents the Lean 4 formalization of a theorem about symmetric log-concave functions on weak compositions. The main result states that such functions are maximized on balanced vectors and minimized on concentrated vectors.
The primary application is to descendant integrals on moduli spaces of curves:
1.2 Definitions
A weak composition of \(d\) into \(n\) parts is an \(n\)-tuple \(e = (e_1, \ldots , e_n) \in \mathbb {Z}^n\) such that:
\(\sum _{i=1}^n e_i = d\)
\(e_i \geq 0\) for all \(i\)
We denote the set of such tuples by \(E(n,d)\).
A weak composition \(e \in E(n,d)\) is balanced if \(|e_i - e_j| \leq 1\) for all \(i, j \in \{ 1, \ldots , n\} \).
A weak composition \(e \in E(n,d)\) is concentrated if there exists \(k\) such that \(e = d \cdot \delta _k\), i.e., all mass is on a single index.
A function \(D : E(n,d) \to \mathbb {Q}\) is \(S_n\)-symmetric if \(D(e \circ \sigma ^{-1}) = D(e)\) for all permutations \(\sigma \in S_n\).
A function \(D : E(n,d) \to \mathbb {Q}\) is log-concave if for all \(e \in E(n,d)\) and indices \(i \neq j\) with \(e_i \geq 1\) and \(e_j \geq 1\):
(The conditions \(e_i \geq 1\) and \(e_j \geq 1\) ensure both modified vectors remain in \(E(n,d)\).)
A symmetric log-concave function on \(E(n,d)\) is a function \(D : E(n,d) \to \mathbb {Q}\) satisfying:
\(S_n\)-symmetry
Log-concavity
Strict positivity: \(D(e) {\gt} 0\) for all \(e\)
1.3 Main Result
Let \(D : E(n,d) \to \mathbb {Q}\) be a function satisfying:
\(S_n\)-symmetry: \(D(e \circ \sigma ^{-1}) = D(e)\) for all permutations \(\sigma \)
Log-concavity: \(D(e)^2 \geq D(e - \delta _i + \delta _j) \cdot D(e + \delta _i - \delta _j)\) for all \(i \neq j\) with \(e_i, e_j \geq 1\)
Strict positivity: \(D(e) {\gt} 0\) for all \(e\)
Then:
Maximum: There exists a balanced vector \(b \in E(n,d)\) such that \(D(e) \leq D(b)\) for all \(e \in E(n,d)\).
Minimum: There exists a concentrated vector \(c \in E(n,d)\) such that \(D(c) \leq D(e)\) for all \(e \in E(n,d)\).
1.4 Key Lemmas and Theorems
Let \(D\) be a symmetric log-concave function on \(E(n,d)\). Then there exists a balanced vector \(b \in E(n,d)\) such that \(D(e) \leq D(b)\) for all \(e \in E(n,d)\).
Let \(D\) be a symmetric log-concave function on \(E(n,d)\). Then there exists a concentrated vector \(c \in E(n,d)\) such that \(D(c) \leq D(e)\) for all \(e \in E(n,d)\).
If a sequence is log-concave and palindromic, then it is unimodal (non-decreasing up to the middle, then non-increasing).
For a symmetric log-concave function \(D\) and any \(e \in E(n,d)\), there exists a balanced \(b \in E(n,d)\) with \(D(e) \leq D(b)\).
For a symmetric log-concave function \(D\) and any \(e \in E(n,d)\), there exists a concentrated \(c \in E(n,d)\) with \(D(c) \leq D(e)\).