Helper Lemmas for the Main Theorem

This file contains the core lemmas needed to prove the main theorem about symmetric log-concave functions on weak compositions.

Main results

• unimodal_of_logconcave_palindromic: Log-concave palindromic sequences are unimodal.
• balanced_maximizes: Any weak composition can be improved to a balanced one.
• concentrated_minimizes: Any weak composition can be reduced to a concentrated one.
• exists_balanced_maximizer: There exists a balanced vector maximizing D.
• exists_concentrated_minimizer: There exists a concentrated vector minimizing D.

Implementation notes

The proofs use well-founded recursion on the "imbalance" measure (sum of squares) for the maximization direction, and on d - maxEntry for the minimization direction.

Slice Analysis Definitions

@[simp]

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

Evaluation of concentrated at its concentration point.

@[simp]

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

Evaluation of concentrated away from its concentration point.

Key Lemma: Log-concave palindromic sequences are unimodal

Imbalance measure for termination

Slice Analysis

Main Theorems

MaxEntry for termination of concentrated_minimizes

theorem SymmetricLogConcaveFunction.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).

theorem SymmetricLogConcaveFunction.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).