Pentagonal number theorem with Franklin's bijective proof

This file proves the pentagonal number theorem at pentagonalNumberTheorem in terms of formal power series:

$$\prod_{n=1}^{\infty} (1 - x^n) = \sum_{k=-\infty}^{\infty} (-1)^k x^{k(3k-1)/2}$$

following Franklin's bijective proof presented on the wikipedia page. This long proof is obsolete by the shorter ones in PowerSeries.lean and Complex.lean, but I keep it here to show case how a combinatorial proof can be done.

Basic properties of pentagonal numbers

def pentagonal'' (k : ℤ) : ℤ

Pentagonal numbers, including negative inputs

Equations

• pentagonal'' k = k * (3 * k - 1) / 2

theorem two_pentagonal'' (k : ℤ) : 2 * pentagonal'' k = k * (3 * k - 1)

Because integer division is hard to work with, we often multiply it by two

theorem pentagonal_nonneg'' (k : ℤ) : 0 ≤ pentagonal'' k

Nonnegativity

theorem two_pentagonal_inj'' {x y : ℤ} (h : x * (3 * x - 1) = y * (3 * y - 1)) : x = y

theorem pentagonal_injective'' : Function.Injective pentagonal''

There are no repeated pentagonal number

def pentagonalDelta (n : ℤ) : ℤ

The inverse of pentagonal number $n = k(3k - 1) / 2$ is $$ k = \frac{1 \pm \sqrt{1 + 24n}}{6} $$ We can use $1 + 24n$ to determine whether such inverse exists.

Equations

• pentagonalDelta n = 1 + 24 * n

theorem pentagonalDelta_pentagonal (k : ℤ) : pentagonalDelta (pentagonal'' k) = (6 * k - 1) ^ 2

def phiCoeff (n : ℤ) : ℤ

The first definition of $\phi(x)$, where each coefficient is assigned according to the pentagonal number inverse. $0$ if there is no inverse; $(-1)^k$ if there is an inverse $k$.

Equations

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

theorem phiCoeff_pentagonal (k : ℤ) : phiCoeff (pentagonal'' k) = ↑k.negOnePow

The coefficients are exactly $(-1)^k$ at pentagonal numbers.

theorem phiCoeff_eq_zero_iff (n : ℤ) : phiCoeff n = 0 ↔ n ∉ Set.range pentagonal''

A coefficient is zero iff and only if it is not a pentagonal number.

def phi : PowerSeries ℤ

$\phi(x)$ is constructed using the coefficients defined above.

Equations

• phi = PowerSeries.mk fun (x : ℕ) => phiCoeff ↑x

theorem hasSum_phi : HasSum (fun (k : ℤ) => (PowerSeries.monomial (pentagonal'' k).toNat) ↑k.negOnePow) phi

The second definition of $\phi(x)$, summing over terms with pentagonal exponents directly.

Some utility of lists

theorem List.zipIdx_set {α : Type u_1} {l : List α} {n k : ℕ} {a : α} : (l.set n a).zipIdx k = (l.zipIdx k).set n (a, n + k)

theorem List.zipIdx_take {α : Type u_1} {l : List α} {n k : ℕ} : (take n l).zipIdx k = take n (l.zipIdx k)

theorem List.zipIdx_drop {α : Type u_1} {l : List α} {n k : ℕ} : (drop n l).zipIdx (k + n) = drop n (l.zipIdx k)

def List.lengthWhile {α : Type u_1} (p : α → Prop) [DecidablePred p] : List α → ℕ

Returns the number of leading elements satisfying a condition.

Equations

• List.lengthWhile p [] = 0
• List.lengthWhile p (x_1 :: xs) = if p x_1 then List.lengthWhile p xs + 1 else 0

@[simp]

theorem List.lengthWhile_nil {α : Type u_1} (p : α → Prop) [DecidablePred p] : lengthWhile p [] = 0

theorem List.lengthWhile_le_length {α : Type u_1} (p : α → Prop) [DecidablePred p] (l : List α) : lengthWhile p l ≤ l.length

theorem List.lengthWhile_eq_length_iff {α : Type u_1} {p : α → Prop} [DecidablePred p] {l : List α} : lengthWhile p l = l.length ↔ Forall p l

theorem List.pred_of_lt_lengthWhile {α : Type u_1} (p : α → Prop) [DecidablePred p] {l : List α} {i : ℕ} (h : i < lengthWhile p l) : p l[i]

theorem List.lengthWhile_eq_iff_of_lt_length {α : Type u_1} {p : α → Prop} [DecidablePred p] {l : List α} {a : ℕ} (ha : a < l.length) : lengthWhile p l = a ↔ (∀ (i : ℕ) (h : i < a), p l[i]) ∧ ¬p l[a]

theorem List.lengthWhile_mono {α : Type u_1} (p : α → Prop) [DecidablePred p] (l r : List α) : lengthWhile p l ≤ lengthWhile p (l ++ r)

theorem List.lengthWhile_set {α : Type u_1} (p : α → Prop) [DecidablePred p] (l : List α) {i : ℕ} (hi : i < l.length) (hp : ¬p l[i]) (x : α) : lengthWhile p l ≤ lengthWhile p (l.set i x)

def List.updateLast {α : Type u_1} (l : List α) (f : α → α) : List α

Replace the last element a with f a.

Equations

• [].updateLast f = []
• (x_1 :: xs).updateLast f = (x_1 :: xs).set ((x_1 :: xs).length - 1) (f ((x_1 :: xs).getLast ⋯))

@[simp]

theorem List.updateLast_id {α : Type u_1} (l : List α) : l.updateLast id = l

theorem List.updateLast_eq_self {α : Type u_1} (l : List α) (f : α → α) (hl : l ≠ []) (h : f (l.getLast hl) = l.getLast hl) : l.updateLast f = l

@[simp]

theorem List.updateLast_nil {α : Type u_1} (f : α → α) : [].updateLast f = []

@[simp]

theorem List.updateLast_eq {α : Type u_1} (l : List α) (f : α → α) (h : l ≠ []) : l.updateLast f = l.set (l.length - 1) (f (l.getLast h))

@[simp]

theorem List.updateLast_eq_nil_iff {α : Type u_1} (l : List α) (f : α → α) : l.updateLast f = [] ↔ l = []

@[simp]

theorem List.getLast_updateLast {α : Type u_1} (l : List α) (f : α → α) (h : l ≠ []) : (l.updateLast f).getLast ⋯ = f (l.getLast h)

@[simp]

theorem List.length_updateLast {α : Type u_1} (l : List α) (f : α → α) : (l.updateLast f).length = l.length

@[simp]

theorem List.updateLast_updateLast {α : Type u_1} (l : List α) (f g : α → α) : (l.updateLast f).updateLast g = l.updateLast (g ∘ f)

theorem List.getElem_updateLast {α : Type u_1} (l : List α) (f : α → α) {i : ℕ} (h : i + 1 < l.length) : (l.updateLast f)[i] = l[i]

Ferrers diagram

A FerrersDiagram n is a representation of distinct partition of number n.

To represent a partition, we first sort all parts in descending order, such as

26 = 14 + 8 + 3 + 1  →  [14, 8, 3, 1]

We then calculate the difference between each element, and keep the last element:

[14, 8, 3, 1]  →  [6, 5, 2, 1]

We get a valid x : FerrersDiagram 26 where x.delta = [6, 5, 2, 1].

structure FerrersDiagram (n : ℕ) : Type

• delta : List ℕ

  The difference between parts.

• delta_pos : List.Forall (fun (x : ℕ) => 0 < x) self.delta

  since we require distinct partition, all delta should be positive.

• delta_sum : (List.map (fun (p : ℕ × ℕ) => p.1 * p.2) (self.delta.zipIdx 1)).sum = n

  All parts should sum back to n. Since we took the difference, this becomes a rolling sum.

theorem FerrersDiagram.ext {n : ℕ} {x y : FerrersDiagram n} (delta : x.delta = y.delta) : x = y

theorem FerrersDiagram.ext_iff {n : ℕ} {x y : FerrersDiagram n} : x = y ↔ x.delta = y.delta

def instReprFerrersDiagram.repr {n✝ : ℕ} : FerrersDiagram n✝ → ℕ → Std.Format

Equations

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

instance instReprFerrersDiagram {n✝ : ℕ} : Repr (FerrersDiagram n✝)

Equations

• instReprFerrersDiagram = { reprPrec := instReprFerrersDiagram.repr }

theorem FerrersDiagram.length_delta_le_n {n : ℕ} (x : FerrersDiagram n) : x.delta.length ≤ n

There can't be more parts than n

theorem FerrersDiagram.delta_ne_nil {n : ℕ} (hn : 0 < n) (x : FerrersDiagram n) : x.delta ≠ []

The parts are not empty for non-zero n. We will discuss mostly with this condition, leaving the n = 0 case a special one for later.

theorem FerrersDiagram.getLast_delta_le_n {n : ℕ} (hn : 0 < n) (x : FerrersDiagram n) : x.delta.getLast ⋯ ≤ n

All parts are not greater than n. Since the last element of delta equals to the smallest part, it is not greater either.

Pentagonal configuration

There is a type of distinct partition we will call "pentagonal". Later, we will see they are in correspondence with pentagonal numbers.

def FerrersDiagram.IsPosPentagonal {n : ℕ} (hn : 0 < n) (x : FerrersDiagram n) : Prop

The special configuration corresponding to pentagonal number n with a positive k.

For example when n = 12, this looks like

∘ ∘ ∘ ∘ ∘
∘ ∘ ∘ ∘
∘ ∘ ∘

Equations

• FerrersDiagram.IsPosPentagonal hn x = (x.delta.getLast ⋯ = x.delta.length ∧ ∀ (i : ℕ) (h : i < x.delta.length - 1), x.delta[i] = 1)

def FerrersDiagram.IsNegPentagonal {n : ℕ} (hn : 0 < n) (x : FerrersDiagram n) : Prop

The special configuration corresponding to pentagonal number n with a negative k.

For example when n = 15, this looks like

∘ ∘ ∘ ∘ ∘ ∘
∘ ∘ ∘ ∘ ∘
∘ ∘ ∘ ∘

Equations

• FerrersDiagram.IsNegPentagonal hn x = (x.delta.getLast ⋯ = x.delta.length + 1 ∧ ∀ (i : ℕ) (h : i < x.delta.length - 1), x.delta[i] = 1)

"Up" and "Down" movement

We will define two operations on distinct partitions / Ferrers diagram:

• down: Take the elements on the right-most 45 degree diagonal and put them to a new bottom row
• up: Take the elements on the bottom row and spread them to the leading rows, forming the new right-most 45 degree diagonal

It is obvious that they are inverse to each other. We will only allow the operation when it is legal to do so. We will then show that for non-pentagonal configurations, either up or down will be legal, and performing the action will make the other one legal.

def FerrersDiagram.diagSize {n : ℕ} (x : FerrersDiagram n) : ℕ

The number of consecutive leading 1 in delta.

This is mimicking the "number of elements in the rightmost 45 degree line of the diagram" s, where we have diagSize = s - 1. However, if the configuration is a complete triangle (i.e. delta are all 1), then we actually have diagSize = s. This inconsistency turns out insignificant, because we only care whether this size is smaller than the smallest part, and that's never the case for triangle configuration regardless which definition we take (except for pentagonal configuration, which we will discuss separately anyway)

Equations

• x.diagSize = List.lengthWhile (fun (x : ℕ) => x = 1) x.delta

@[reducible, inline]

abbrev FerrersDiagram.takeDiagFun (delta : List ℕ) (i : ℕ) (hi : i < delta.length) : List ℕ

Equations

• FerrersDiagram.takeDiagFun delta i hi = delta.set i (delta[i] - 1)

def FerrersDiagram.takeDiag {n : ℕ} (x : FerrersDiagram n) (i : ℕ) (hi : i < x.delta.length) (h : 1 < x.delta[i]) : FerrersDiagram (n - (i + 1))

The action to subtract one from the first i + 1 parts.

Equations

• x.takeDiag i hi h = { delta := FerrersDiagram.takeDiagFun x.delta i hi, delta_pos := ⋯, delta_sum := ⋯ }

theorem FerrersDiagram.takeDiag_ne_nil {n : ℕ} (x : FerrersDiagram n) (i : ℕ) (hi : i < x.delta.length) (h : 1 < x.delta[i]) : (x.takeDiag i hi h).delta ≠ []

theorem FerrersDiagram.getLast_takeDiag {n : ℕ} (x : FerrersDiagram n) (i : ℕ) (hi : i < x.delta.length - 1) (h : 1 < x.delta[i]) : (x.takeDiag i ⋯ h).delta.getLast ⋯ = x.delta.getLast ⋯

takeDiag preserves the last part as long as we didn't touch it.

theorem FerrersDiagram.getLast_takeDiag' {n : ℕ} (hn : 0 < n) (x : FerrersDiagram n) (i : ℕ) (hi : i = x.delta.length - 1) (h : 1 < x.delta[i]) : (x.takeDiag i ⋯ h).delta.getLast ⋯ = x.delta.getLast ⋯ - 1

takeDiag make the last part smaller by one if we took one from every part

@[reducible, inline]

abbrev FerrersDiagram.putLastFun (delta : List ℕ) (i : ℕ) : List ℕ

Equations

• FerrersDiagram.putLastFun delta i = (delta.updateLast fun (x : ℕ) => x - (i + 1)) ++ [i + 1]

def FerrersDiagram.putLast {n : ℕ} (hn : 0 < n) (x : FerrersDiagram n) (i : ℕ) (hi : i + 1 < x.delta.getLast ⋯) : FerrersDiagram (n + (i + 1))

The action to add a new part smaller than every other part.

Equations

• FerrersDiagram.putLast hn x i hi = { delta := FerrersDiagram.putLastFun x.delta i, delta_pos := ⋯, delta_sum := ⋯ }

theorem FerrersDiagram.getLast_putLast {n : ℕ} (hn : 0 < n) (x : FerrersDiagram n) (i : ℕ) (hi : i + 1 < x.delta.getLast ⋯) : (putLast hn x i hi).delta.getLast ⋯ = i + 1

putLast updates the last part.

theorem FerrersDiagram.diagSize_putLast {n : ℕ} (hn : 0 < n) (x : FerrersDiagram n) (i : ℕ) (hi : i + 1 < x.delta.getLast ⋯) (hlast : 1 < x.delta.getLast ⋯) : x.diagSize ≤ (putLast hn x i hi).diagSize

putLast increases or preserves diagSize.

def FerrersDiagram.IsToDown {n : ℕ} (hn : 0 < n) (x : FerrersDiagram n) : Prop

The criteria to legally move the diagonal down

Equations

• FerrersDiagram.IsToDown hn x = (x.diagSize + 1 < x.delta.getLast ⋯)

instance FerrersDiagram.instDecidableIsToDown {n : ℕ} (hn : 0 < n) (x : FerrersDiagram n) : Decidable (IsToDown hn x)

Equations

• FerrersDiagram.instDecidableIsToDown hn x = id inferInstance

theorem FerrersDiagram.diagSize_of_isToDown {n : ℕ} (hn : 0 < n) (x : FerrersDiagram n) (hdown : IsToDown hn x) : x.diagSize + 1 < n

theorem FerrersDiagram.diagSize_of_isToDown' {n : ℕ} (hn : 0 < n) (x : FerrersDiagram n) (hdown : IsToDown hn x) : n = n - (x.diagSize + 1) + (x.diagSize + 1)

theorem FerrersDiagram.diagSize_lt_length {n : ℕ} (hn : 0 < n) (x : FerrersDiagram n) (hdown : IsToDown hn x) : x.diagSize < x.delta.length

theorem FerrersDiagram.delta_diagSize {n : ℕ} (hn : 0 < n) (x : FerrersDiagram n) (hdown : IsToDown hn x) : 1 < x.delta[x.diagSize]

def FerrersDiagram.takeDiag' {n : ℕ} (hn : 0 < n) (x : FerrersDiagram n) (hdown : IsToDown hn x) : FerrersDiagram (n - (x.diagSize + 1))

Specialize takeDiag to take precisely the 45 degree diagonal.

Equations

• FerrersDiagram.takeDiag' hn x hdown = x.takeDiag x.diagSize ⋯ ⋯

theorem FerrersDiagram.diagSize_add_one_lt {n : ℕ} (hn : 0 < n) (x : FerrersDiagram n) (hdown : IsToDown hn x) (hnegpen : ¬IsNegPentagonal hn x) : x.diagSize + 1 < (takeDiag' hn x hdown).delta.getLast ⋯

def FerrersDiagram.down {n : ℕ} (hn : 0 < n) (x : FerrersDiagram n) (hdown : IsToDown hn x) (hnegpen : ¬IsNegPentagonal hn x) : FerrersDiagram n

The down action is defined as takeDiag then putLast.

Equations

• FerrersDiagram.down hn x hdown hnegpen = ⋯.mpr (FerrersDiagram.putLast ⋯ (FerrersDiagram.takeDiag' hn x hdown) x.diagSize ⋯)

theorem FerrersDiagram.delta_down {n : ℕ} (hn : 0 < n) (x : FerrersDiagram n) (hdown : IsToDown hn x) (hnegpen : ¬IsNegPentagonal hn x) : (down hn x hdown hnegpen).delta = putLastFun (takeDiagFun x.delta x.diagSize ⋯) x.diagSize

theorem FerrersDiagram.getLast_down {n : ℕ} (hn : 0 < n) (x : FerrersDiagram n) (hdown : IsToDown hn x) (hnegpen : ¬IsNegPentagonal hn x) : (down hn x hdown hnegpen).delta.getLast ⋯ = x.diagSize + 1

theorem FerrersDiagram.length_down {n : ℕ} (hn : 0 < n) (x : FerrersDiagram n) (hdown : IsToDown hn x) (hnegpen : ¬IsNegPentagonal hn x) : (down hn x hdown hnegpen).delta.length = x.delta.length + 1

theorem FerrersDiagram.down_notToDown {n : ℕ} (hn : 0 < n) (x : FerrersDiagram n) (hdown : IsToDown hn x) (hnegpen : ¬IsNegPentagonal hn x) : ¬IsToDown hn (down hn x hdown hnegpen)

Barring pentagonal configuration, doing down will make it illegal to down.

theorem FerrersDiagram.down_notPosPentagonal {n : ℕ} (hn : 0 < n) (x : FerrersDiagram n) (hdown : IsToDown hn x) (hnegpen : ¬IsNegPentagonal hn x) : ¬IsPosPentagonal hn (down hn x hdown hnegpen)

Non-pentagonal configuration will not be positive-pentagonal after down.

theorem FerrersDiagram.down_notNegPentagonal {n : ℕ} (hn : 0 < n) (x : FerrersDiagram n) (hdown : IsToDown hn x) (hnegpen : ¬IsNegPentagonal hn x) : ¬IsNegPentagonal hn (down hn x hdown hnegpen)

Non-pentagonal configuration will not be negative-pentagonal after down.

@[reducible, inline]

abbrev FerrersDiagram.takeLastFun (delta : List ℕ) (h : delta ≠ []) : List ℕ

Equations

• FerrersDiagram.takeLastFun delta h = (List.take (delta.length - 1) delta).updateLast fun (x : ℕ) => x + delta.getLast h

def FerrersDiagram.takeLast {n : ℕ} (hn : 0 < n) (x : FerrersDiagram n) : FerrersDiagram (n - x.delta.getLast ⋯)

The inverse of putLast

Equations

• FerrersDiagram.takeLast hn x = { delta := FerrersDiagram.takeLastFun x.delta ⋯, delta_pos := ⋯, delta_sum := ⋯ }

theorem FerrersDiagram.length_takeLast {n : ℕ} (hn : 0 < n) (x : FerrersDiagram n) : (takeLast hn x).delta.length = x.delta.length - 1

@[reducible, inline]

abbrev FerrersDiagram.putDiagFun (delta : List ℕ) (i : ℕ) (hi : i < delta.length) : List ℕ

Equations

• FerrersDiagram.putDiagFun delta i hi = delta.set i (delta[i] + 1)

def FerrersDiagram.putDiag {n : ℕ} (x : FerrersDiagram n) (i : ℕ) (hi : i < x.delta.length) : FerrersDiagram (n + (i + 1))

The inverse of takeDiag.

Equations

• x.putDiag i hi = { delta := FerrersDiagram.putDiagFun x.delta i hi, delta_pos := ⋯, delta_sum := ⋯ }

theorem FerrersDiagram.aux_up_size {n : ℕ} (hn : 0 < n) (x : FerrersDiagram n) : n - x.delta.getLast ⋯ + (x.delta.getLast ⋯ - 1 + 1) = n

theorem FerrersDiagram.getLast_lt_of_notToDown {n : ℕ} (hn : 0 < n) (x : FerrersDiagram n) (hdown : ¬IsToDown hn x) (hpospen : ¬IsPosPentagonal hn x) : x.delta.getLast ⋯ < x.delta.length

theorem FerrersDiagram.getLast_lt_of_notToDown' {n : ℕ} (hn : 0 < n) (x : FerrersDiagram n) (hdown : ¬IsToDown hn x) (hpospen : ¬IsPosPentagonal hn x) : x.delta.getLast ⋯ - 1 < (takeLast hn x).delta.length

def FerrersDiagram.up {n : ℕ} (hn : 0 < n) (x : FerrersDiagram n) (hdown : ¬IsToDown hn x) (hpospen : ¬IsPosPentagonal hn x) : FerrersDiagram n

The inverse of down.

Equations

• FerrersDiagram.up hn x hdown hpospen = ⋯.mp ((FerrersDiagram.takeLast hn x).putDiag (x.delta.getLast ⋯ - 1) ⋯)

theorem FerrersDiagram.delta_up {n : ℕ} (hn : 0 < n) (x : FerrersDiagram n) (hdown : ¬IsToDown hn x) (hpospen : ¬IsPosPentagonal hn x) : (up hn x hdown hpospen).delta = putDiagFun (takeLastFun x.delta ⋯) (x.delta.getLast ⋯ - 1) ⋯

theorem FerrersDiagram.one_lt_length {n : ℕ} (hn : 0 < n) (x : FerrersDiagram n) (hdown : ¬IsToDown hn x) (hpospen : ¬IsPosPentagonal hn x) : 1 < x.delta.length

theorem FerrersDiagram.diagSize_up {n : ℕ} (hn : 0 < n) (x : FerrersDiagram n) (hdown : ¬IsToDown hn x) (hpospen : ¬IsPosPentagonal hn x) : (up hn x hdown hpospen).diagSize = x.delta.getLast ⋯ - 1

theorem FerrersDiagram.getLast_up {n : ℕ} (hn : 0 < n) (x : FerrersDiagram n) (hdown : ¬IsToDown hn x) (hpospen : ¬IsPosPentagonal hn x) : x.delta.getLast ⋯ < (up hn x hdown hpospen).delta.getLast ⋯

theorem FerrersDiagram.up_isToDown {n : ℕ} (hn : 0 < n) (x : FerrersDiagram n) (hdown : ¬IsToDown hn x) (hpospen : ¬IsPosPentagonal hn x) : IsToDown hn (up hn x hdown hpospen)

Barring pentagonal configuration, doing up will make it legal to do down.

theorem FerrersDiagram.length_up {n : ℕ} (hn : 0 < n) (x : FerrersDiagram n) (hdown : ¬IsToDown hn x) (hpospen : ¬IsPosPentagonal hn x) : (up hn x hdown hpospen).delta.length = x.delta.length - 1

theorem FerrersDiagram.up_notPentagonal {n : ℕ} (hn : 0 < n) (x : FerrersDiagram n) (hdown : ¬IsToDown hn x) (hpospen : ¬IsPosPentagonal hn x) (h : ∀ (i : ℕ) (h : i < (up hn x hdown hpospen).delta.length - 1), (up hn x hdown hpospen).delta[i] = 1) : (up hn x hdown hpospen).delta.length + 1 < (up hn x hdown hpospen).delta.getLast ⋯

Non-pentagonal configuration will not be pentagonal after doing up.

Here we disprove the common condition of both pos- and neg- pentagonal.

theorem FerrersDiagram.up_notPosPentagonal {n : ℕ} (hn : 0 < n) (x : FerrersDiagram n) (hdown : ¬IsToDown hn x) (hpospen : ¬IsPosPentagonal hn x) : ¬IsPosPentagonal hn (up hn x hdown hpospen)

theorem FerrersDiagram.up_notNegPentagonal {n : ℕ} (hn : 0 < n) (x : FerrersDiagram n) (hdown : ¬IsToDown hn x) (hpospen : ¬IsPosPentagonal hn x) : ¬IsNegPentagonal hn (up hn x hdown hpospen)

theorem FerrersDiagram.takeLastFun_putLastFun (delta : List ℕ) (i : ℕ) (hdelta : delta ≠ []) (h : i + 1 ≤ delta.getLast hdelta) : takeLastFun (putLastFun delta i) ⋯ = delta

theorem FerrersDiagram.putLastFun_takeLastFun (delta : List ℕ) (hdelta : delta ≠ []) (hpos : List.Forall (fun (x : ℕ) => 0 < x) delta) : putLastFun (takeLastFun delta hdelta) (delta.getLast hdelta - 1) = delta

theorem FerrersDiagram.takeDiagFun_putDiagFun (delta : List ℕ) (i : ℕ) (hi : i < delta.length) : takeDiagFun (putDiagFun delta i hi) i ⋯ = delta

theorem FerrersDiagram.up_down {n : ℕ} (hn : 0 < n) (x : FerrersDiagram n) (hdown : IsToDown hn x) (hnegpen : ¬IsNegPentagonal hn x) : up hn (down hn x hdown hnegpen) ⋯ ⋯ = x

up is the left inverse of down.

theorem FerrersDiagram.down_up {n : ℕ} (hn : 0 < n) (x : FerrersDiagram n) (hdown : ¬IsToDown hn x) (hpospen : ¬IsPosPentagonal hn x) : down hn (up hn x hdown hpospen) ⋯ ⋯ = x

up is the right inverse of down.

Up/down involution

We now combine both up and down into one function bij, selecting the operation based on which way is legal. We notice that in either way the parity of delta.length is changed, so this provides a bijection between even and odd non-pentagonal configurations.

theorem FerrersDiagram.parity_up {n : ℕ} (hn : 0 < n) (x : FerrersDiagram n) (hdown : ¬IsToDown hn x) (hpospen : ¬IsPosPentagonal hn x) : Even (up hn x hdown hpospen).delta.length ↔ ¬Even x.delta.length

theorem FerrersDiagram.parity_down {n : ℕ} (hn : 0 < n) (x : FerrersDiagram n) (hdown : IsToDown hn x) (hnegpen : ¬IsNegPentagonal hn x) : Even (down hn x hdown hnegpen).delta.length ↔ ¬Even x.delta.length

def FerrersDiagram.bij {n : ℕ} (hn : 0 < n) (x : FerrersDiagram n) (hpospen : ¬IsPosPentagonal hn x) (hnegpen : ¬IsNegPentagonal hn x) : FerrersDiagram n

bij is either up or down, depending on which way is legal.

Equations

• FerrersDiagram.bij hn x hpospen hnegpen = if hdown : FerrersDiagram.IsToDown hn x then FerrersDiagram.down hn x hdown hnegpen else FerrersDiagram.up hn x hdown hpospen

theorem FerrersDiagram.bij_notPosPentagonal {n : ℕ} (hn : 0 < n) (x : FerrersDiagram n) (hpospen : ¬IsPosPentagonal hn x) (hnegpen : ¬IsNegPentagonal hn x) : ¬IsPosPentagonal hn (bij hn x hpospen hnegpen)

theorem FerrersDiagram.bij_notNegPentagonal {n : ℕ} (hn : 0 < n) (x : FerrersDiagram n) (hpospen : ¬IsPosPentagonal hn x) (hnegpen : ¬IsNegPentagonal hn x) : ¬IsNegPentagonal hn (bij hn x hpospen hnegpen)

@[reducible, inline]

abbrev FerrersDiagram.NpFerrers {n : ℕ} (hn : 0 < n) : Type

Type of all non-pentagonal Ferrers diagrams.

Equations

• FerrersDiagram.NpFerrers hn = { x : FerrersDiagram n // ¬FerrersDiagram.IsPosPentagonal hn x ∧ ¬FerrersDiagram.IsNegPentagonal hn x }

@[reducible, inline]

abbrev FerrersDiagram.bijNp {n : ℕ} {hn : 0 < n} (x : NpFerrers hn) : NpFerrers hn

bij as a function on NpFerrers.

Equations

• FerrersDiagram.bijNp x = ⟨FerrersDiagram.bij hn ↑x ⋯ ⋯, ⋯⟩

@[simp]

theorem FerrersDiagram.bijNp_bijNp {n : ℕ} {hn : 0 < n} (x : NpFerrers hn) : bijNp (bijNp x) = x

theorem FerrersDiagram.parity_bijNp {n : ℕ} {hn : 0 < n} (x : NpFerrers hn) : Even (↑(bijNp x)).delta.length ↔ ¬Even (↑x).delta.length

@[reducible, inline]

abbrev FerrersDiagram.NpEven {n : ℕ} (hn : 0 < n) : Set (NpFerrers hn)

Even non-pentagonal configurations.

Equations

• FerrersDiagram.NpEven hn = {x : FerrersDiagram.NpFerrers hn | Even (↑x).delta.length}

@[reducible, inline]

abbrev FerrersDiagram.NpOdd {n : ℕ} (hn : 0 < n) : Set (NpFerrers hn)

Odd non-pentagonal configurations.

Equations

• FerrersDiagram.NpOdd hn = {x : FerrersDiagram.NpFerrers hn | ¬Even (↑x).delta.length}

theorem FerrersDiagram.NpEven_eq {n : ℕ} (hn : 0 < n) : NpEven hn = {x : { x : FerrersDiagram n // ¬IsPosPentagonal hn x ∧ ¬IsNegPentagonal hn x } | ↑x ∈ {x : FerrersDiagram n | Even x.delta.length}}

theorem FerrersDiagram.NpOdd_eq {n : ℕ} (hn : 0 < n) : NpOdd hn = {x : { x : FerrersDiagram n // ¬IsPosPentagonal hn x ∧ ¬IsNegPentagonal hn x } | ↑x ∈ {x : FerrersDiagram n | ¬Even x.delta.length}}

theorem FerrersDiagram.NpFerrers_card_eq {n : ℕ} (hn : 0 < n) : (NpEven hn).ncard = (NpOdd hn).ncard

theorem FerrersDiagram.card_eq {n : ℕ} (hn : 0 < n) : {x : FerrersDiagram n | (¬IsPosPentagonal hn x ∧ ¬IsNegPentagonal hn x) ∧ Even x.delta.length}.ncard = {x : FerrersDiagram n | (¬IsPosPentagonal hn x ∧ ¬IsNegPentagonal hn x) ∧ ¬Even x.delta.length}.ncard

The numer of even and odd configurations, barring pentagonal ones, are equal.

Translate Ferrers diagram to distinct partition

def FerrersDiagram.foldDelta : List ℕ → List ℕ

Unbundled function that calculates parts from delta.

Equations

• FerrersDiagram.foldDelta [] = []
• FerrersDiagram.foldDelta (x' :: xs') = match FerrersDiagram.foldDelta xs' with | [] => [x'] | x'_1 :: xs' => (x'_1 + x') :: x'_1 :: xs'

@[simp]

theorem FerrersDiagram.foldDelta_eq_nil {l : List ℕ} : foldDelta l = [] ↔ l = []

@[simp]

theorem FerrersDiagram.length_foldDelta (l : List ℕ) : (foldDelta l).length = l.length

theorem FerrersDiagram.foldDelta_pos_of_pos {l : List ℕ} (hpos : ∀ a ∈ l, 0 < a) (a : ℕ) : a ∈ foldDelta l → 0 < a

theorem FerrersDiagram.head_foldDelta (l : List ℕ) : (foldDelta l).headI = l.sum

theorem FerrersDiagram.sum_foldDelta (l : List ℕ) : (foldDelta l).sum = (List.map (fun (p : ℕ × ℕ) => p.1 * p.2) (l.zipIdx 1)).sum

theorem FerrersDiagram.foldDelta_sorted (l : List ℕ) : List.Pairwise (fun (x1 x2 : ℕ) => x1 ≥ x2) (foldDelta l)

theorem FerrersDiagram.foldDelta_sorted_of_pos {l : List ℕ} (hpos : List.Forall (fun (x : ℕ) => 0 < x) l) : List.Pairwise (fun (x1 x2 : ℕ) => x1 > x2) (foldDelta l)

@[simp]

theorem FerrersDiagram.mergeSort_foldDelta (l : List ℕ) : ((foldDelta l).mergeSort fun (x1 x2 : ℕ) => decide (x1 ≥ x2)) = foldDelta l

def FerrersDiagram.unfoldDelta : List ℕ → List ℕ

Unbundled function that calculates delta from parts.

Equations

• FerrersDiagram.unfoldDelta [] = []
• FerrersDiagram.unfoldDelta [x_1] = [x_1]
• FerrersDiagram.unfoldDelta (x_1 :: y :: xs) = (x_1 - y) :: FerrersDiagram.unfoldDelta (y :: xs)

@[simp]

theorem FerrersDiagram.length_unfoldDelta (l : List ℕ) : (unfoldDelta l).length = l.length

theorem FerrersDiagram.unfoldDelta_pos_of_sorted {l : List ℕ} (hsort : List.Pairwise (fun (x1 x2 : ℕ) => x1 > x2) l) (hpos : List.Forall (fun (x : ℕ) => 0 < x) l) : List.Forall (fun (x : ℕ) => 0 < x) (unfoldDelta l)

theorem FerrersDiagram.sum_unfoldDelta' {l : List ℕ} (hsort : List.Pairwise (fun (x1 x2 : ℕ) => x1 ≥ x2) l) : (unfoldDelta l).sum = l.headI

theorem FerrersDiagram.sum_unfoldDelta {l : List ℕ} (hsort : List.Pairwise (fun (x1 x2 : ℕ) => x1 ≥ x2) l) : (List.map (fun (p : ℕ × ℕ) => p.1 * p.2) ((unfoldDelta l).zipIdx 1)).sum = l.sum

@[simp]

theorem FerrersDiagram.unfoldDelta_foldDelta (l : List ℕ) : unfoldDelta (foldDelta l) = l

@[simp]

theorem FerrersDiagram.foldDelta_unfoldDelta {l : List ℕ} (h : List.Pairwise (fun (x1 x2 : ℕ) => x1 ≥ x2) l) : foldDelta (unfoldDelta l) = l

theorem FerrersDiagram.Multiset.qind {α : Type u_1} {motive : Multiset α → Prop} (mk : ∀ (a : List α), motive ↑a) (a : Multiset α) : motive a

def FerrersDiagram.equivPartitionDistincts (n : ℕ) : FerrersDiagram n ≃ ↥(Nat.Partition.distincts n)

Correspondence between FerrersDiagram n and Nat.Partition.distincts n, which also preserves parity.

Equations

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

instance FerrersDiagram.instFintype {n : ℕ} : Fintype (FerrersDiagram n)

Equations

• FerrersDiagram.instFintype = Fintype.ofEquiv (↥(Nat.Partition.distincts n)) (FerrersDiagram.equivPartitionDistincts n).symm

@[simp]

theorem FerrersDiagram.equivPartitionDistincts_even {n : ℕ} (x : FerrersDiagram n) : Even (↑((equivPartitionDistincts n) x)).parts.card ↔ Even x.delta.length

@[simp]

theorem FerrersDiagram.equivPartitionDistincts_symm_even {n : ℕ} (x : ↥(Nat.Partition.distincts n)) : Even ((equivPartitionDistincts n).symm x).delta.length ↔ Even (↑x).parts.card

theorem FerrersDiagram.card_sub {n : ℕ} (hn : 0 < n) : ↑{x : FerrersDiagram n | Even x.delta.length}.ncard - ↑{x : FerrersDiagram n | ¬Even x.delta.length}.ncard = ↑{x : FerrersDiagram n | (IsPosPentagonal hn x ∨ IsNegPentagonal hn x) ∧ Even x.delta.length}.ncard - ↑{x : FerrersDiagram n | (IsPosPentagonal hn x ∨ IsNegPentagonal hn x) ∧ ¬Even x.delta.length}.ncard

The difference between even and odd partitions is reduced to pentagonal cases.

theorem FerrersDiagram.Finset.sum_range_id_mul_two' (n : ℕ) : 2 * ∑ i ∈ Finset.range n, ↑i = ↑n * (↑n - 1)

theorem FerrersDiagram.negpenSum {k : ℕ} (hk : 0 < k) : 2 * ↑(List.map (fun (p : ℕ × ℕ) => p.1 * p.2) ((List.replicate (k - 1) 1 ++ [k + 1]).zipIdx 1)).sum = -↑k * (3 * -↑k - 1)

Calculation of n for negative pentagonal case.

theorem FerrersDiagram.pospenSum {k : ℕ} (hk : 0 < k) : 2 * ↑(List.map (fun (p : ℕ × ℕ) => p.1 * p.2) ((List.replicate (k - 1) 1 ++ [k]).zipIdx 1)).sum = ↑k * (3 * ↑k - 1)

Calculation of n for positive pentagonal case.

theorem FerrersDiagram.IsPosPentagonal.two_n_eq {n : ℕ} (hn : 0 < n) (x : FerrersDiagram n) (hpospen : IsPosPentagonal hn x) : 2 * ↑n = ↑x.delta.length * (3 * ↑x.delta.length - 1)

For positive pentagonal case, delta.length = k.

theorem FerrersDiagram.IsNegPentagonal.two_n_eq {n : ℕ} (hn : 0 < n) (x : FerrersDiagram n) (hpospen : IsNegPentagonal hn x) : 2 * ↑n = -↑x.delta.length * (3 * -↑x.delta.length - 1)

For negative pentagonal case, delta.length = -k.

theorem FerrersDiagram.pentagonal_exists_k {n : ℕ} (hn : 0 < n) (x : FerrersDiagram n) (hpen : IsPosPentagonal hn x ∨ IsNegPentagonal hn x) : ∃ (k : ℤ), 2 * ↑n = k * (3 * k - 1) ∧ (Even x.delta.length ↔ Even k)

In summary, pentagonal case always gives a pentagonal number n.

theorem FerrersDiagram.pentagonal_of_exists_k {n : ℕ} (hn : 0 < n) {k : ℤ} (h : 2 * ↑n = k * (3 * k - 1)) : ∃ (x : FerrersDiagram n), IsPosPentagonal hn x ∨ IsNegPentagonal hn x

The converse: pentagonal number n gives a pentagonal case.

theorem FerrersDiagram.pentagonal_subsingleton {n : ℕ} (hn : 0 < n) : {x : FerrersDiagram n | IsPosPentagonal hn x ∨ IsNegPentagonal hn x}.Subsingleton

There is at most one pentagonal case for a given n.

theorem FerrersDiagram.phiCoeff_eq_card_sub {n : ℕ} (hn : 0 < n) : phiCoeff ↑n = ↑{x : FerrersDiagram n | (IsPosPentagonal hn x ∨ IsNegPentagonal hn x) ∧ Even x.delta.length}.ncard - ↑{x : FerrersDiagram n | (IsPosPentagonal hn x ∨ IsNegPentagonal hn x) ∧ ¬Even x.delta.length}.ncard

Third definition of $\phi$: coefficients represents the existence of even and odd pentagonal partition.

Final connection

def phiCoeff' (n : ℕ) : ℤ

Forth definition: of $\phi$: coefficients represents the difference of even and odd partitions.

Equations

• phiCoeff' n = ∑ s ∈ Nat.Partition.distincts n, (-1) ^ s.parts.card

theorem phiCoeff_eq (n : ℕ) : phiCoeff ↑n = phiCoeff' n

theorem eularPhi : HasProd (fun (n : ℕ+) => 1 - (PowerSeries.monomial ↑n) 1) (PowerSeries.mk fun (x : ℕ) => phiCoeff' x)

The multiplication formula of $\phi(x)$ expands precisely to the partition formula.

theorem pentagonalNumberTheorem : ∏' (n : ℕ+), (1 - (PowerSeries.monomial ↑n) 1) = ∑' (k : ℤ), (PowerSeries.monomial (k * (3 * k - 1) / 2).toNat) ↑((-1) ^ k)

Pentagonal number theorem

$$\prod_{n=1}^{\infty} (1 - x^n) = \sum_{k=-\infty}^{\infty} (-1)^k x^{k(3k-1)/2}$$