Balanced Vector Optimization

Main Statement (Theorem Blueprint)

This file formalizes the following result:

Theorem. Let D : E(n,d) → ℚ₊ be a function on weak compositions (n-tuples of non-negative integers summing to d) satisfying:

1. Sₙ-Symmetry: D(e ∘ σ⁻¹) = D(e) for all permutations σ
2. Log-concavity condition: D(e)² ≥ D(e - δᵢ + δⱼ) · D(e + δᵢ - δⱼ) for all i ≠ j with eᵢ, eⱼ ≥ 1
3. Strict positivity: D(e) > 0 for all e

Then:

• (Maximum) D is maximized on balanced vectors (where |eᵢ - eⱼ| ≤ 1 for all i,j)
• (Minimum) D is minimized on concentrated vectors (where e = d·δₖ for some k)

Key Definitions (for verification)

Definition	Location	Informal meaning
WeakComposition n d	line 128	n-tuple e : Fin n → ℤ with ∑eᵢ = d, eᵢ ≥ 0
IsBalanced e	line 214	∀ i j, eᵢ ≤ eⱼ + 1 ∧ eⱼ ≤ eᵢ + 1
IsConcentrated d e	line 218	∃ k, eᵢ = if i = k then d else 0
IsSymmetric D	line 400	D(e ∘ σ⁻¹) = D(e) for all σ ∈ Sₙ
SatisfiesLogConcavity D	line 409	the log-concavity condition above
IsStrictlyPositive D	line 415	D(e) > 0 for all e

Main Theorems (for verification)

Paper-style formulation (recommended for citation):

Theorem	Location	Statement
main_theorem_paper	line 1238	Combined: ∃ balanced max ∧ ∃ concentrated min
exists_balanced_maximizer	line 1183	∃ b, IsBalanced b ∧ ∀ e, D(e) ≤ D(b)
exists_concentrated_minimizer	line 1210	∃ c, IsConcentrated c ∧ ∀ e, D(c) ≤ D(e)

Original formulation (pointwise):

Theorem	Location	Statement
main_theorem	line 1166	∀ e, ∃ bal with D(e) ≤ D(bal) ∧ vice versa
maximized_on_balanced	line 1139	∀ e, ∃ e', IsBalanced e' ∧ D(e) ≤ D(e')
minimized_on_concentrated	line 1153	∀ e, ∃ e', IsConcentrated e' ∧ D(e') ≤ D(e)

Supporting structure:

Definition	Location	Purpose
SymmetricLogConcaveFunction	line 1117	Bundles D with its three properties

Implementation (used by the above):

Theorem	Location	Statement
balanced_maximizes	line 718	Core proof for maximum result
concentrated_minimizes	line 1022	Core proof for minimum result

Proof Strategy

1. Slice analysis: For fixed i ≠ j, the "slice sequence" s(t) = D(composition with eᵢ = t, eⱼ = q - t) is shown to be log-concave and palindromic.

2. Unimodality lemma (unimodal_of_logconcave_palindromic, line 306): Log-concave palindromic sequences on [0,q] are unimodal (increasing then decreasing around q/2).

3. Balancing increases D: When eᵢ - eⱼ ≥ 2, the modification eᵢ ↦ eᵢ - 1, eⱼ ↦ eⱼ + 1 moves toward the midpoint of the slice, increasing D.

4. Concentrating decreases D: When eⱼ ≤ eᵢ, moving mass from j to i moves away from the midpoint, decreasing D.

5. Termination: Balancing uses imbalance ∑ eᵢ² (decreases strictly). Concentrating uses d - maxEntry(e) (decreases strictly until maxEntry = d).

Reusable sum lemma for two-point updates

theorem sum_ite_ite_eq_add_add_sum_erase_erase {n : ℕ} (f : Fin n → ℤ) (i j : Fin n) (hij : i ≠ j) (a b : ℤ) : (∑ k : Fin n, if k = i then a else if k = j then b else f k) = a + b + ∑ k ∈ (Finset.univ.erase i).erase j, f k

Key lemma: extract two positions from a sum with nested if-then-else.

Weak Compositions (using ℤ for easier arithmetic)

structure WeakComposition (n : ℕ) (d : ℤ) : Type

A weak composition of d into n parts is a vector e : Fin n → ℤ with ∑ eᵢ = d and all entries non-negative.

• toFun : Fin n → ℤ
• sum_eq : ∑ i : Fin n, self.toFun i = d
• nonneg (i : Fin n) : 0 ≤ self.toFun i

instance WeakComposition.instCoeFunForallFinInt {n : ℕ} {d : ℤ} : CoeFun (WeakComposition n d) fun (x : WeakComposition n d) => Fin n → ℤ

Equations

• WeakComposition.instCoeFunForallFinInt = { coe := WeakComposition.toFun }

theorem WeakComposition.ext {n : ℕ} {d : ℤ} {e e' : WeakComposition n d} (h : ∀ (i : Fin n), e.toFun i = e'.toFun i) : e = e'

theorem WeakComposition.ext_iff {n : ℕ} {d : ℤ} {e e' : WeakComposition n d} : e = e' ↔ ∀ (i : Fin n), e.toFun i = e'.toFun i

def WeakComposition.concentrated {n : ℕ} {d : ℤ} (hd : 0 ≤ d) (k : Fin n) : WeakComposition n d

The concentrated vector: all zeros except d at position k.

Equations

• WeakComposition.concentrated hd k = { toFun := fun (i : Fin n) => if i = k then d else 0, sum_eq := ⋯, nonneg := ⋯ }

@[simp]

theorem WeakComposition.concentrated_at {n : ℕ} {d : ℤ} (hd : 0 ≤ d) (k : Fin n) : (concentrated hd k).toFun k = d

@[simp]

theorem WeakComposition.concentrated_ne {n : ℕ} {d : ℤ} (hd : 0 ≤ d) (k j : Fin n) (h : j ≠ k) : (concentrated hd k).toFun j = 0

theorem WeakComposition.sum_modify_eq {n : ℕ} {d : ℤ} {e : Fin n → ℤ} {i j : Fin n} (hij : i ≠ j) (hsum : ∑ k : Fin n, e k = d) : (∑ k : Fin n, if k = i then e i - 1 else if k = j then e j + 1 else e k) = d

Auxiliary: the sum of a function that modifies two positions. This captures: if we change e at i to (e i - 1) and at j to (e j + 1), the total sum is preserved.

def WeakComposition.modify {n : ℕ} {d : ℤ} (e : WeakComposition n d) (i j : Fin n) (hi : 1 ≤ e.toFun i) (hij : i ≠ j) : WeakComposition n d

Modify a composition by transferring one unit from position i to position j.

Equations

• e.modify i j hi hij = { toFun := fun (k : Fin n) => if k = i then e.toFun i - 1 else if k = j then e.toFun j + 1 else e.toFun k, sum_eq := ⋯, nonneg := ⋯ }

@[simp]

theorem WeakComposition.modify_at_i {n : ℕ} {d : ℤ} (e : WeakComposition n d) (i j : Fin n) (hi : 1 ≤ e.toFun i) (hij : i ≠ j) : (e.modify i j hi hij).toFun i = e.toFun i - 1

@[simp]

theorem WeakComposition.modify_at_j {n : ℕ} {d : ℤ} (e : WeakComposition n d) (i j : Fin n) (hi : 1 ≤ e.toFun i) (hij : i ≠ j) : (e.modify i j hi hij).toFun j = e.toFun j + 1

@[simp]

theorem WeakComposition.modify_at_other {n : ℕ} {d : ℤ} (e : WeakComposition n d) (i j k : Fin n) (hi : 1 ≤ e.toFun i) (hij : i ≠ j) (hki : k ≠ i) (hkj : k ≠ j) : (e.modify i j hi hij).toFun k = e.toFun k

Balanced and Concentrated Vectors

def IsBalanced {n : ℕ} (e : Fin n → ℤ) : Prop

A vector is balanced if all entries differ by at most 1.

Equations

• IsBalanced e = ∀ (i j : Fin n), e i ≤ e j + 1 ∧ e j ≤ e i + 1

def IsConcentrated {n : ℕ} (d : ℤ) (e : Fin n → ℤ) : Prop

A vector is concentrated if it equals d • δₖ for some k.

Equations

• IsConcentrated d e = ∃ (k : Fin n), ∀ (i : Fin n), e i = if i = k then d else 0

Finiteness of Weak Compositions

theorem WeakComposition.entry_le_d {n : ℕ} {d : ℤ} (e : WeakComposition n d) (i : Fin n) : e.toFun i ≤ d

Each entry of a weak composition is bounded by d.

instance WeakComposition.finite {n : ℕ} {d : ℤ} (hd : 0 ≤ d) : Finite (WeakComposition n d)

The domain WeakComposition n d is finite when d ≥ 0. Each entry satisfies 0 ≤ e i ≤ d, so we can inject into Fin n → Fin (d.toNat + 1).

theorem WeakComposition.nonempty {n : ℕ} {d : ℤ} (hn : 0 < n) (hd : 0 ≤ d) : Nonempty (WeakComposition n d)

WeakComposition n d is nonempty when n > 0 and d ≥ 0.

Log-Concave and Palindromic Sequences

def LogConcaveOn (s : ℤ → ℚ) (q : ℤ) : Prop

A sequence s : ℤ → ℚ is log-concave on [0, q].

Equations

• LogConcaveOn s q = ∀ (t : ℤ), 1 ≤ t → t ≤ q - 1 → s t ^ 2 ≥ s (t - 1) * s (t + 1)

def IsPalindromicOn (s : ℤ → ℚ) (q : ℤ) : Prop

A sequence is palindromic on [0, q].

Equations

• IsPalindromicOn s q = ∀ (t : ℤ), 0 ≤ t → t ≤ q → s t = s (q - t)

def IsPositiveOn (s : ℤ → ℚ) (q : ℤ) : Prop

A sequence is positive on [0, q].

Equations

• IsPositiveOn s q = ∀ (t : ℤ), 0 ≤ t → t ≤ q → 0 < s t

Key Lemma: Log-concave palindromic sequences are unimodal

theorem unimodal_of_logconcave_palindromic {s : ℤ → ℚ} {q : ℤ} (hq : 0 ≤ q) (hpos : IsPositiveOn s q) (hlc : LogConcaveOn s q) (hpal : IsPalindromicOn s q) : (∀ (t : ℤ), 0 ≤ t → 2 * t < q → s t ≤ s (t + 1)) ∧ ∀ (t : ℤ), 2 * t > q → t ≤ q → s t ≤ s (t - 1)

The main unimodality lemma.

The Main Theorem Setup

def IsSymmetric {n : ℕ} {d : ℤ} (D : WeakComposition n d → ℚ) : Prop

A function on weak compositions that is symmetric under the Sₙ action.

Equations

• IsSymmetric D = ∀ (σ : Equiv.Perm (Fin n)) (e : WeakComposition n d), D { toFun := e.toFun ∘ ⇑(Equiv.symm σ), sum_eq := ⋯, nonneg := ⋯ } = D e

def SatisfiesLogConcavity {n : ℕ} {d : ℤ} (D : WeakComposition n d → ℚ) : Prop

The log-concavity condition for D.

Equations

• SatisfiesLogConcavity D = ∀ (e : WeakComposition n d) (i j : Fin n) (hij : i ≠ j) (hi : 1 ≤ e.toFun i) (hj : 1 ≤ e.toFun j), D e ^ 2 ≥ D (e.modify i j hi hij) * D (e.modify j i hj ⋯)

def IsStrictlyPositive {n : ℕ} {d : ℤ} (D : WeakComposition n d → ℚ) : Prop

D is strictly positive.

Equations

• IsStrictlyPositive D = ∀ (e : WeakComposition n d), 0 < D e

Imbalance measure for termination

def imbalance {n : ℕ} (e : Fin n → ℤ) : ℤ

The "imbalance" of a vector: sum of squares.

Equations

• imbalance e = ∑ i : Fin n, e i ^ 2

theorem sq_transfer_decreases {a b : ℤ} (h : a ≥ b + 2) : (a - 1) ^ 2 + (b + 1) ^ 2 < a ^ 2 + b ^ 2

Key algebraic fact: (a-1)² + (b+1)² < a² + b² when a ≥ b + 2.

theorem imbalance_decreases {n : ℕ} {d : ℤ} (e : WeakComposition n d) (i j : Fin n) (hij : i ≠ j) (hi : 1 ≤ e.toFun i) (hdiff : e.toFun j + 2 ≤ e.toFun i) : imbalance (e.modify i j hi hij).toFun < imbalance e.toFun

If e_i ≥ e_j + 2, then modifying from i to j decreases imbalance.

theorem exists_imbalanced_pair {n : ℕ} (e : Fin n → ℤ) (h : ¬IsBalanced e) : ∃ (i : Fin n) (j : Fin n), i ≠ j ∧ e j + 2 ≤ e i

If a vector is not balanced, there exist i, j with e_i ≥ e_j + 2.

Slice Analysis

theorem sum_slice_eq {n : ℕ} {d : ℤ} {e : Fin n → ℤ} {i j : Fin n} (hij : i ≠ j) (hsum : ∑ k : Fin n, e k = d) (t : ℤ) : (∑ k : Fin n, if k = i then t else if k = j then e i + e j - t else e k) = d

Auxiliary: sum is preserved when we put t at position i and (q-t) at position j.

def sliceComposition {n : ℕ} {d : ℤ} (e : WeakComposition n d) (i j : Fin n) (hij : i ≠ j) (t : ℤ) (ht : 0 ≤ t) (htq : t ≤ e.toFun i + e.toFun j) : WeakComposition n d

Given a weak composition e and distinct positions i, j, construct the composition with value t at position i and (e_i + e_j - t) at position j.

Equations

• sliceComposition e i j hij t ht htq = { toFun := fun (k : Fin n) => if k = i then t else if k = j then e.toFun i + e.toFun j - t else e.toFun k, sum_eq := ⋯, nonneg := ⋯ }

noncomputable def sliceSeq {n : ℕ} {d : ℤ} (D : WeakComposition n d → ℚ) (e : WeakComposition n d) (i j : Fin n) (hij : i ≠ j) : ℤ → ℚ

The slice sequence for D.

Equations

• sliceSeq D e i j hij t = if h : 0 ≤ t ∧ t ≤ e.toFun i + e.toFun j then D (sliceComposition e i j hij t ⋯ ⋯) else 0

theorem sliceSeq_palindromic {n : ℕ} {d : ℤ} (D : WeakComposition n d → ℚ) (hsym : IsSymmetric D) (e : WeakComposition n d) (i j : Fin n) (hij : i ≠ j) : IsPalindromicOn (sliceSeq D e i j hij) (e.toFun i + e.toFun j)

The slice sequence is palindromic when D is symmetric.

theorem sliceSeq_logconcave {n : ℕ} {d : ℤ} (D : WeakComposition n d → ℚ) (hlc : SatisfiesLogConcavity D) (e : WeakComposition n d) (i j : Fin n) (hij : i ≠ j) : LogConcaveOn (sliceSeq D e i j hij) (e.toFun i + e.toFun j)

The slice sequence is log-concave when D satisfies log-concavity.

theorem sliceSeq_positive {n : ℕ} {d : ℤ} (D : WeakComposition n d → ℚ) (hpos : IsStrictlyPositive D) (e : WeakComposition n d) (i j : Fin n) (hij : i ≠ j) : IsPositiveOn (sliceSeq D e i j hij) (e.toFun i + e.toFun j)

The slice sequence is positive when D is positive.

Main Theorems

theorem balancing_increases_D {n : ℕ} {d : ℤ} (D : WeakComposition n d → ℚ) (hpos : IsStrictlyPositive D) (hsym : IsSymmetric D) (hlc : SatisfiesLogConcavity D) (e : WeakComposition n d) (i j : Fin n) (hij : i ≠ j) (hi : 1 ≤ e.toFun i) (hdiff : e.toFun j + 2 ≤ e.toFun i) : D e ≤ D (e.modify i j hi hij)

The balancing step weakly increases D when entries differ by ≥ 2.

theorem imbalance_nonneg {n : ℕ} {d : ℤ} (e : WeakComposition n d) : 0 ≤ imbalance e.toFun

Imbalance is non-negative for weak compositions.

theorem balanced_maximizes {n : ℕ} {d : ℤ} (D : WeakComposition n d → ℚ) (hpos : IsStrictlyPositive D) (hsym : IsSymmetric D) (hlc : SatisfiesLogConcavity D) (e : WeakComposition n d) : ∃ (e' : WeakComposition n d), IsBalanced e'.toFun ∧ D e ≤ D e'

Any vector can be transformed to a balanced vector while increasing D.

theorem concentrating_decreases_D {n : ℕ} {d : ℤ} (D : WeakComposition n d → ℚ) (hpos : IsStrictlyPositive D) (hsym : IsSymmetric D) (hlc : SatisfiesLogConcavity D) (e : WeakComposition n d) (i j : Fin n) (hij : i ≠ j) (hj : 1 ≤ e.toFun j) (hdiff : e.toFun j < e.toFun i) : D (e.modify j i hj ⋯) ≤ D e

When e_i > e_j, moving mass from j to i (concentrating) decreases D.

MaxEntry for termination of concentrated_minimizes

noncomputable def maxEntry {n : ℕ} (e : Fin n → ℤ) (hn : 0 < n) : ℤ

The maximum entry of a vector.

Equations

• maxEntry e hn = (Finset.image e Finset.univ).max' ⋯

theorem exists_eq_maxEntry {n : ℕ} (e : Fin n → ℤ) (hn : 0 < n) : ∃ (i : Fin n), e i = maxEntry e hn

theorem le_maxEntry {n : ℕ} (e : Fin n → ℤ) (hn : 0 < n) (i : Fin n) : e i ≤ maxEntry e hn

theorem WeakComposition.maxEntry_le_d {n : ℕ} {d : ℤ} (e : WeakComposition n d) (hn : 0 < n) : maxEntry e.toFun hn ≤ d

theorem WeakComposition.concentrated_of_entry_eq_d {n : ℕ} {d : ℤ} (e : WeakComposition n d) (i : Fin n) (hi : e.toFun i = d) : IsConcentrated d e.toFun

If some entry equals d, then the composition is concentrated at that index.

theorem WeakComposition.concentrated_of_maxEntry_eq_d {n : ℕ} {d : ℤ} (e : WeakComposition n d) (hn : 0 < n) (hmax : maxEntry e.toFun hn = d) : IsConcentrated d e.toFun

theorem WeakComposition.maxEntry_modify_to_maximizer {n : ℕ} {d : ℤ} (e : WeakComposition n d) (hn : 0 < n) (i j : Fin n) (hij : i ≠ j) (hj : 1 ≤ e.toFun j) (hiMax : e.toFun i = maxEntry e.toFun hn) : maxEntry (e.modify j i hj ⋯).toFun hn = maxEntry e.toFun hn + 1

Moving mass to a maximizer increases maxEntry by 1.

theorem WeakComposition.measure_decreases_of_maxEntry_increases {n : ℕ} {d : ℤ} (e e1 : WeakComposition n d) (hn : 0 < n) (hmax : maxEntry e1.toFun hn = maxEntry e.toFun hn + 1) (hmax_lt : maxEntry e.toFun hn < d) : (d - maxEntry e1.toFun hn).toNat < (d - maxEntry e.toFun hn).toNat

def nonzeroCount {n : ℕ} (e : Fin n → ℤ) : ℕ

Count of non-zero entries.

Equations

• nonzeroCount e = {i : Fin n | e i ≠ 0}.card

theorem exists_two_positive {n : ℕ} {d : ℤ} (hd : 0 < d) (e : WeakComposition n d) (h : ¬IsConcentrated d e.toFun) : ∃ (i : Fin n) (j : Fin n), i ≠ j ∧ 0 < e.toFun i ∧ 0 < e.toFun j

If e is not concentrated and d > 0, there exist distinct i, j with e.i > 0 and e.j > 0.

theorem concentrated_minimizes {n : ℕ} {d : ℤ} (hn : 0 < n) (hd : 0 ≤ d) (D : WeakComposition n d → ℚ) (hpos : IsStrictlyPositive D) (hsym : IsSymmetric D) (hlc : SatisfiesLogConcavity D) (e : WeakComposition n d) : ∃ (e' : WeakComposition n d), IsConcentrated d e'.toFun ∧ D e' ≤ D e

Any vector can be transformed to a concentrated vector while decreasing D.

==========================================================================

Main Results (Clean Formulation)

This section provides the main theorems in their cleanest form, suitable for citation and verification against informal statements.

Informal Theorem. Let D : E(n,d) → ℚ₊ be a function on weak compositions satisfying Sₙ-symmetry, the log-concavity condition D(e)² ≥ D(e-δᵢ+δⱼ)·D(e+δᵢ-δⱼ), and strict positivity. Then D is maximized on balanced vectors and minimized on concentrated vectors.

structure SymmetricLogConcaveFunction (n : ℕ) (d : ℤ) : Type

A function D on weak compositions satisfying the three conditions: Sₙ-symmetry, log-concavity, and strict positivity.

• D : WeakComposition n d → ℚ

  The function D : E(n,d) → ℚ

• symmetric : IsSymmetric self.D

  D(e ∘ σ⁻¹) = D(e) for all permutations σ

• logConcave : SatisfiesLogConcavity self.D

  D(e)² ≥ D(e - δᵢ + δⱼ) · D(e + δᵢ - δⱼ) when eᵢ, eⱼ ≥ 1

• strictlyPositive : IsStrictlyPositive self.D

  D(e) > 0 for all e

theorem SymmetricLogConcaveFunction.maximized_on_balanced {n : ℕ} {d : ℤ} (F : SymmetricLogConcaveFunction n d) (e : WeakComposition n d) : ∃ (e' : WeakComposition n d), IsBalanced e'.toFun ∧ F.D e ≤ F.D e'

Main Theorem (Maximum). Every symmetric log-concave function on weak compositions is maximized on balanced vectors.

More precisely: for any e ∈ E(n,d), there exists a balanced e' ∈ E(n,d) with D(e) ≤ D(e').

A vector is balanced if all entries differ by at most 1: ∀ i j, |eᵢ - eⱼ| ≤ 1.

theorem SymmetricLogConcaveFunction.minimized_on_concentrated {n : ℕ} {d : ℤ} (hn : 0 < n) (hd : 0 ≤ d) (F : SymmetricLogConcaveFunction n d) (e : WeakComposition n d) : ∃ (e' : WeakComposition n d), IsConcentrated d e'.toFun ∧ F.D e' ≤ F.D e

Main Theorem (Minimum). Every symmetric log-concave function on weak compositions is minimized on concentrated vectors.

More precisely: for any e ∈ E(n,d), there exists a concentrated e' ∈ E(n,d) with D(e') ≤ D(e).

A vector is concentrated if it equals d · δₖ for some index k.

Requires n > 0 and d ≥ 0.

theorem main_theorem {n : ℕ} {d : ℤ} (hn : 0 < n) (hd : 0 ≤ d) (F : SymmetricLogConcaveFunction n d) : (∀ (e : WeakComposition n d), ∃ (e_bal : WeakComposition n d), IsBalanced e_bal.toFun ∧ F.D e ≤ F.D e_bal) ∧ ∀ (e : WeakComposition n d), ∃ (e_conc : WeakComposition n d), IsConcentrated d e_conc.toFun ∧ F.D e_conc ≤ F.D e

Combined Main Theorem (Original formulation). For any symmetric log-concave function D on weak compositions E(n,d):

• The maximum of D is achieved on balanced vectors
• The minimum of D is achieved on concentrated vectors

theorem exists_balanced_maximizer {n : ℕ} {d : ℤ} (hn : 0 < n) (hd : 0 ≤ d) (F : SymmetricLogConcaveFunction n d) : ∃ (b : WeakComposition n d), IsBalanced b.toFun ∧ ∀ (e : WeakComposition n d), F.D e ≤ F.D b

Main Theorem (Paper formulation - Maximum). There exists a balanced vector that maximizes D over all of E(n,d).

This formulation matches the informal statement: "D is maximized on balanced vectors."

Proof strategy (Option B from GPT-5.2):

1. The domain is finite, so a global maximizer eMax exists
2. By maximized_on_balanced, there's balanced b with D(eMax) ≤ D(b)
3. But eMax is globally maximal, so D(b) ≤ D(eMax)
4. Hence D(b) = D(eMax), and b is a balanced global maximizer

theorem exists_concentrated_minimizer {n : ℕ} {d : ℤ} (hn : 0 < n) (hd : 0 ≤ d) (F : SymmetricLogConcaveFunction n d) : ∃ (c : WeakComposition n d), IsConcentrated d c.toFun ∧ ∀ (e : WeakComposition n d), F.D c ≤ F.D e

Main Theorem (Paper formulation - Minimum). There exists a concentrated vector that minimizes D over all of E(n,d).

This formulation matches the informal statement: "D is minimized on concentrated vectors."

Proof strategy: Same as maximum but with global minimizer.

theorem main_theorem_paper {n : ℕ} {d : ℤ} (hn : 0 < n) (hd : 0 ≤ d) (F : SymmetricLogConcaveFunction n d) : (∃ (b : WeakComposition n d), IsBalanced b.toFun ∧ ∀ (e : WeakComposition n d), F.D e ≤ F.D b) ∧ ∃ (c : WeakComposition n d), IsConcentrated d c.toFun ∧ ∀ (e : WeakComposition n d), F.D c ≤ F.D e

Main Theorem (Paper formulation - Combined). For any symmetric log-concave function D on weak compositions E(n,d):

• There exists a balanced vector b such that D(b) ≥ D(e) for all e
• There exists a concentrated vector c such that D(c) ≤ D(e) for all e

This is the natural formalization matching the paper's statement: "D is maximized on balanced vectors and minimized on concentrated vectors."