Pentagonal Number Theorem — Definitions

Core definitions for the formalization of the Euler Pentagonal Number Theorem via Franklin's involution.

Main definitions

• consecutiveTopRun: length of the maximal consecutive run ending at m in S
• distinctPartitions: partitions of n into distinct positive parts
• distinctPartitionsEven, distinctPartitionsOdd: partitions with an even (resp. odd) number of parts
• pe, po: cardinalities of distinctPartitionsEven n, distinctPartitionsOdd n
• partBase, partMax, partSlope, partSlopeSet: structural invariants of a partition
• distinctPartitionsAlpha, distinctPartitionsBeta, distinctPartitionsSpecial: three-way decomposition of distinctPartitions n by Franklin's involution
• smkSet, spkSet: the special pentagonal partitions S_{−k} and S_k
• alphaOp, betaOp: Franklin's involution maps on distinctPartitionsAlpha and distinctPartitionsBeta

def PentagonalNumberTheorem.Franklin.consecutiveTopRun (S : Finset ℕ) : ℕ → ℕ

The length of the maximal consecutive run of elements of S ending at m, counted downward.

Equations

• PentagonalNumberTheorem.Franklin.consecutiveTopRun S 0 = if 0 ∈ S then 1 else 0
• PentagonalNumberTheorem.Franklin.consecutiveTopRun S m.succ = if m + 1 ∈ S then 1 + PentagonalNumberTheorem.Franklin.consecutiveTopRun S m else 0

def PentagonalNumberTheorem.Franklin.distinctPartitions (n : ℕ) : Finset (Finset ℕ)

The set of subsets S ⊆ {1, …, n} with ∑_{s ∈ S} s = n, i.e., partitions of n into distinct positive parts.

Equations

• PentagonalNumberTheorem.Franklin.distinctPartitions n = {S ∈ (Finset.Icc 1 n).powerset | S.sum id = n}

def PentagonalNumberTheorem.Franklin.distinctPartitionsEven (n : ℕ) : Finset (Finset ℕ)

Partitions of n into distinct positive parts with an even number of parts.

Equations

• PentagonalNumberTheorem.Franklin.distinctPartitionsEven n = {S ∈ PentagonalNumberTheorem.Franklin.distinctPartitions n | S.card % 2 = 0}

def PentagonalNumberTheorem.Franklin.distinctPartitionsOdd (n : ℕ) : Finset (Finset ℕ)

Partitions of n into distinct positive parts with an odd number of parts.

Equations

• PentagonalNumberTheorem.Franklin.distinctPartitionsOdd n = {S ∈ PentagonalNumberTheorem.Franklin.distinctPartitions n | S.card % 2 = 1}

def PentagonalNumberTheorem.Franklin.pe (n : ℕ) : ℕ

Number of partitions of n into an even number of distinct positive parts.

Equations

• PentagonalNumberTheorem.Franklin.pe n = (PentagonalNumberTheorem.Franklin.distinctPartitionsEven n).card

def PentagonalNumberTheorem.Franklin.po (n : ℕ) : ℕ

Number of partitions of n into an odd number of distinct positive parts.

Equations

• PentagonalNumberTheorem.Franklin.po n = (PentagonalNumberTheorem.Franklin.distinctPartitionsOdd n).card

def PentagonalNumberTheorem.Franklin.partBase (S : Finset ℕ) : ℕ

The smallest element of a partition, returning 0 for the empty set.

Equations

• PentagonalNumberTheorem.Franklin.partBase S = if h : S.Nonempty then S.min' h else 0

def PentagonalNumberTheorem.Franklin.partMax (S : Finset ℕ) : ℕ

The largest element of a partition, returning 0 for the empty set.

Equations

• PentagonalNumberTheorem.Franklin.partMax S = if h : S.Nonempty then S.max' h else 0

def PentagonalNumberTheorem.Franklin.partSlope (S : Finset ℕ) : ℕ

The length of the maximal consecutive run from max(S) downward in S.

Equations

• PentagonalNumberTheorem.Franklin.partSlope S = PentagonalNumberTheorem.Franklin.consecutiveTopRun S (PentagonalNumberTheorem.Franklin.partMax S)

def PentagonalNumberTheorem.Franklin.partSlopeSet (S : Finset ℕ) : Finset ℕ

The interval {max(S) − slope(S) + 1, …, max(S)} (the "slope set" of S).

Equations

• One or more equations did not get rendered due to their size.

def PentagonalNumberTheorem.Franklin.distinctPartitionsAlpha (n : ℕ) : Finset (Finset ℕ)

Partitions S ∈ distinctPartitions n that are nonempty and satisfy (b ≤ s ∧ b ∉ D) ∨ b + 1 ≤ s, with b = partBase S, s = partSlope S.

Equations

• One or more equations did not get rendered due to their size.

def PentagonalNumberTheorem.Franklin.distinctPartitionsBeta (n : ℕ) : Finset (Finset ℕ)

Partitions S ∈ distinctPartitions n that are nonempty and satisfy (s < b ∧ b ∉ D) ∨ s + 2 ≤ b, with b = partBase S, s = partSlope S.

Equations

• One or more equations did not get rendered due to their size.

def PentagonalNumberTheorem.Franklin.distinctPartitionsSpecial (n : ℕ) : Finset (Finset ℕ)

Partitions of n into distinct parts that are either empty or satisfy base(S) ∈ slopeSet(S) with base(S) = slope(S) or base(S) = slope(S) + 1.

Equations

• One or more equations did not get rendered due to their size.

def PentagonalNumberTheorem.Franklin.smkSet (k : ℕ) : Finset ℕ

The pentagonal partition S_{−k} = {k, k+1, …, 2k−1} of (3k²−k)/2.

Equations

• PentagonalNumberTheorem.Franklin.smkSet k = Finset.Icc k (2 * k - 1)

def PentagonalNumberTheorem.Franklin.spkSet (k : ℕ) : Finset ℕ

The pentagonal partition S_k = {k+1, k+2, …, 2k} of (3k²+k)/2.

Equations

• PentagonalNumberTheorem.Franklin.spkSet k = Finset.Icc (k + 1) (2 * k)

def PentagonalNumberTheorem.Franklin.alphaOp (S : Finset ℕ) : Finset ℕ

For S ∈ 𝒫_α(n) with base b and max m, α(S) = (S \ {b, m−b+1}) ∪ {m+1}.

Equations

• One or more equations did not get rendered due to their size.

def PentagonalNumberTheorem.Franklin.betaOp (S : Finset ℕ) : Finset ℕ

For S ∈ 𝒫_β(n) with slope s and max m, β(S) = (S ∪ {s, m−s}) \ {m}.

Equations

• One or more equations did not get rendered due to their size.