WARNING

This repo contains AI generated proofs which may contain errors. To trust the claimed main result, and for it to be meaningful to have Lean check the actual proofs you must read, understand, and validate the content of this file.

Weak Compositions and Symmetric Log-Concave Functions

This file defines weak compositions of an integer d into n parts, along with symmetric log-concave functions on the space of weak compositions.

Main definitions

• WeakComposition n d: A vector e : Fin n → ℤ with ∑ eᵢ = d and all entries non-negative.
• SymmetricLogConcaveFunction n d: A function D : WeakComposition n d → ℚ that is Sₙ-symmetric, log-concave, and strictly positive.
• IsBalanced: A vector where all entries differ by at most 1.
• IsConcentrated: A vector with all mass at a single position.

Implementation notes

We use ℤ for entries rather than ℕ to simplify arithmetic in proofs, particularly when dealing with the modify operation that transfers units between positions.

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 → ℤ

  The underlying function from indices to integer values.

• sum_eq : ∑ i : Fin n, self.toFun i = d

  The entries sum to d.

• nonneg (i : Fin n) : 0 ≤ self.toFun i

  All entries are non-negative.

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

Equations

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

def WeakComposition.concentrated {d : ℤ} {n : ℕ} (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 := ⋯ }

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 := ⋯ }

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

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

Auxiliary Definitions for Main Statement

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