Theorems · Theorem · number theory

Pentagonal.tprod_one_sub_pow

∀ {R : Type u_1} [inst : CommRing R] [inst_1 : TopologicalSpace R] [IsTopologicalRing R] [T2Space R] {x : R},
  IsTopologicallyNilpotent x →
    (∀ (k : ℕ), Summable fun n => x ^ ((k + 1) * n) * ∏ i ∈ Finset.range (n + 1), (1 - x ^ (k + i + 1))) →
      (∀ (k : ℕ), Multipliable fun n => 1 - x ^ (n + k + 1)) →
        (Summable fun k => (-1) ^ k * (x ^ pentagonal (-↑k) - x ^ pentagonal (↑k + 1))) →
          Filter.Tendsto
              (fun k =>
                (-1) ^ (k + 1) * x ^ ((k + 1) * (3 * k + 4) / 2) *
                  ∑' (n : ℕ), x ^ ((k + 1) * n) * ∏ i ∈ Finset.range (n + 1), (1 - x ^ (k + i + 1)))
              Filter.atTop (nhds 0) →
            ∏' (n : ℕ), (1 - x ^ (n + 1)) = ∑' (k : ℕ), (-1) ^ k * (x ^ pentagonal (-↑k) - x ^ pentagonal (↑k + 1))

Pentagonal number theorem, assuming appropriate multipliability and summability. $$ \prod_{n = 0}^{\infty} (1 - x^{n + 1}) = \sum_{k=0}^{\infty} (-1)^k \left(x^{k(3k+1)/2} - x^{(k+1)(3k+2)/2}\right) $$

Defined in

Mathlib.Combinatorics.Enumerative.Pentagonal.Ring

Cited by

0 results in Mathlib

Foundations

Depth 100 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

CommRingTopologicalSpaceIsTopologicalRingT2Space