address comments

Author: wwylele

Mathlib/RingTheory/PowerSeries/Pentagonal.lean

@@ -15,7 +15,7 @@ import Mathlib.Topology.Algebra.InfiniteSum.Pentagonal
 
 This file proves the pentagonal number theorem for power series:
 
-$$ \prod_{n = 0}^{\infty} 1 - x^{n + 1} = \sum_{k=-\infty}^{\infty} (-1)^k x^{a_k} $$
+$$ \prod_{n = 0}^{\infty} (1 - x^{n + 1}) = \sum_{k=-\infty}^{\infty} (-1)^k x^{a_k} $$
 
 where $a_k = k(3k - 1)/2$ are the pentagonal numbers.
 
@@ -97,7 +97,7 @@ theorem summable_pow_pentagonal_sub : Summable fun (k : ℕ) ↦
 
 /-- **Pentagonal number theorem** for power series, summing over natural numbers:
 
-$$ \prod_{n = 0}^{\infty} 1 - x^{n + 1} =
+$$ \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) $$ -/
 theorem tprod_one_sub_X_pow_eq_tsum_nat [IsTopologicalRing R] [T2Space R] :
     ∏' n, (1 - X ^ (n + 1) : R⟦X⟧) =
@@ -137,7 +137,7 @@ exponent $a_{-k}$ where $a_k = k(3k - 1)/2$ are the generalized pentagonal numbe
 Note that $a_{-k} = (-k)(3(-k) - 1)/2 = k(3k + 1)/2$, which explains the exponent in the
 following formula:
 
-$$ \prod_{n = 0}^{\infty} 1 - x^{n + 1} = \sum_{k=-\infty}^{\infty} (-1)^k x^{k(3k + 1)/2} $$ -/
+$$ \prod_{n = 0}^{\infty} (1 - x^{n + 1}) = \sum_{k=-\infty}^{\infty} (-1)^k x^{k(3k + 1)/2} $$ -/
 theorem tprod_one_sub_X_pow' [IsTopologicalRing R] [T2Space R] :
     ∏' n, (1 - X ^ (n + 1)) = ∑' k, (Int.negOnePow k : R⟦X⟧) * X ^ (k * (3 * k + 1) / 2).toNat := by
   rw [← tsum_nat_add_neg_add_one (summable_pow_pentagonal' R), tprod_one_sub_X_pow_eq_tsum_nat]
@@ -158,7 +158,7 @@ theorem summable_pow_pentagonal [IsTopologicalRing R] :
 /-- **Pentagonal number theorem** for power series, summing over integers written using the
 exponent $a_k$ where $a_k = k(3k - 1)/2$ are the generalized pentagonal numbers:
 
-$$ \prod_{n = 0}^{\infty} 1 - x^{n + 1} = \sum_{k=-\infty}^{\infty} (-1)^k x^{k(3k - 1)/2} $$ -/
+$$ \prod_{n = 0}^{\infty} (1 - x^{n + 1}) = \sum_{k=-\infty}^{\infty} (-1)^k x^{k(3k - 1)/2} $$ -/
 theorem tprod_one_sub_X_pow [IsTopologicalRing R] [T2Space R] :
     ∏' n, (1 - X ^ (n + 1)) = ∑' k, (Int.negOnePow k : R⟦X⟧) * X ^ (k * (3 * k - 1) / 2).toNat := by
   rw [tprod_one_sub_X_pow', ← neg_injective.tsum_eq (by simp)]

Mathlib/Topology/Algebra/InfiniteSum/Pentagonal.lean

@@ -39,13 +39,14 @@ $$ a_{k, n} = x^{(k+1)n} \prod_{i=0}^{n} 1 - x^{k + i + 1} $$
 We will also use its sum
 
 $$ A_k = \sum_{n=0}^{\infty} a_{k, n} $$ -/
-public abbrev powMulProdOneSubPow (k n : ℕ) (x : R) : R :=
+@[expose]
+public def powMulProdOneSubPow (k n : ℕ) (x : R) : R :=
   x ^ ((k + 1) * n) * ∏ i ∈ Finset.range (n + 1), (1 - x ^ (k + i + 1))
 
 /-- And a second auxiliary sequence
 
 $$ b_{k, n} = x^{(k+1)n} (x^{2k + n + 3} - 1) \prod_{i=0}^{n-1} 1 - x^{k + i + 2} $$ -/
-abbrev aux (k n : ℕ) (x : R) : R :=
+def aux (k n : ℕ) (x : R) : R :=
   x ^ ((k + 1) * n) * (x ^ (2 * k + n + 3) - 1) * ∏ i ∈ Finset.range n, (1 - x ^ (k + i + 2))
 
 /-- `powMulProdOneSubPow` and `aux` have relation
@@ -85,7 +86,7 @@ theorem tsum_powMulProdOneSubPow (k : ℕ) {x : R} (hx : IsTopologicallyNilpoten
 
 /-- The Euler function is related to $A_0$ by
 
-$$ \prod_{n = 0}^{\infty} 1 - x^{n + 1} = 1 - x - x^2 A_0 $$ -/
+$$ \prod_{n = 0}^{\infty} (1 - x^{n + 1}) = 1 - x - x^2 A_0 $$ -/
 theorem tprod_one_sub_pow_eq_powMulProdOneSubPow_zero {x : R}
     (hsum : ∀ k, Summable (powMulProdOneSubPow k · x))
     (h : ∀ k, Multipliable fun n ↦ 1 - x ^ (n + k + 1)) :
@@ -108,7 +109,7 @@ theorem tprod_one_sub_pow_eq_powMulProdOneSubPow_zero {x : R}
 
 /-- Applying the recurrence formula repeatedly, we get
 
-$$ \prod_{n = 0}^{\infty} 1 - x^{n + 1} =
+$$ \prod_{n = 0}^{\infty} (1 - x^{n + 1}) =
 \left(\sum_{k=0}^{j} (-1)^k \left(x^{k(3k+1)/2} - x^{(k+1)(3k+2)/2}\right) \right) +
 (-1)^{j+1}x^{(j+1)(3j+4)/2}A_j $$ -/
 theorem tprod_one_sub_pow_eq_powMulProdOneSubPow (j : ℕ) {x : R} (hx : IsTopologicallyNilpotent x)
@@ -137,7 +138,7 @@ theorem tprod_one_sub_pow_eq_powMulProdOneSubPow (j : ℕ) {x : R} (hx : IsTopol
 
 /-- Pentagonal number theorem, assuming appropriate multipliability and summability.
 
-$$ \prod_{n = 0}^{\infty} 1 - x^{n + 1} =
+$$ \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) $$ -/
 public theorem tprod_one_sub_pow {x : R} (hx : IsTopologicallyNilpotent x)
     (hsum : ∀ k, Summable (powMulProdOneSubPow k · x))