Pentagonal numbers

This file introduces (generalized) pentagonal numbers $k(3k-1)/2$ for integer $k$.

Some sources, such as A001318 in the OEIS, order generalized pentagonal numbers by indices $k = 0, 1, -1, 2, -2, \cdots$ to form a strictly monotone sequence. This file doesn't follow this convention, but implicitly shows the monotonicity in pentagonal_lt_pentagonal_neg and pentagonal_neg_lt_pentagonal_add_one.

Main definitions

• pentagonal: pentagonal numbers as a function ℤ → ℕ.

TODO

Show the relation between pentagonal numbers and partitions, including the pentagonal number theorem.

References

• https://en.wikipedia.org/wiki/Pentagonal_number

def pentagonal (k : ℤ) : ℕ

Pentagonal numbers $k(3k-1)/2$ for integer $k$.

Equations

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

theorem pentagonal_def (k : ℤ) : pentagonal k = (k * (3 * k - 1) / 2).toNat

theorem pentagonal_neg (k : ℤ) : pentagonal (-k) = (k * (3 * k + 1) / 2).toNat

theorem natCast_pentagonal (k : ℤ) : ↑(pentagonal k) = k * (3 * k - 1) / 2

theorem two_mul_natCast_pentagonal (k : ℤ) : 2 * ↑(pentagonal k) = k * (3 * k - 1)

theorem two_mul_natCast_pentagonal_neg (k : ℤ) : 2 * ↑(pentagonal (-k)) = k * (3 * k + 1)

theorem pentagonal_injective : Function.Injective pentagonal

@[simp]

theorem pentagonal_inj {x y : ℤ} : pentagonal x = pentagonal y ↔ x = y

theorem pentagonal_lt_pentagonal_neg {k : ℤ} (h : 0 < k) : pentagonal k < pentagonal (-k)

theorem pentagonal_neg_lt_pentagonal_add_one {k : ℤ} (h : 0 ≤ k) : pentagonal (-k) < pentagonal (k + 1)

theorem pentagonal_strictMonoOn : StrictMonoOn pentagonal (Set.Ici 0)

theorem pentagonal_strictAntiOn : StrictAntiOn pentagonal (Set.Iic 0)