Not ready yet. Merge master

Author: wwylele

Mathlib/RingTheory/PowerSeries/Pentagonal.lean

@@ -6,6 +6,7 @@ Authors: Weiyi Wang
 module
 
 public import Mathlib.Algebra.Ring.NegOnePow
+public import Mathlib.Combinatorics.Enumerative.Pentagonal
 public import Mathlib.RingTheory.PowerSeries.PiTopology
 
 import Mathlib.Topology.Algebra.InfiniteSum.Pentagonal
@@ -41,55 +42,11 @@ left-hand side.
   topology on the ring.
 -/
 
-public section PublicPentagonalNumber
-theorem two_pentagonal (k : ℤ) : 2 * (k * (3 * k - 1) / 2) = k * (3 * k - 1) := by
-  refine Int.two_mul_ediv_two_of_even ?_
-  obtain h | h := Int.even_or_odd k
-  · exact Even.mul_right h (3 * k - 1)
-  · refine Even.mul_left (Int.even_sub_one.mpr (Int.not_even_iff_odd.mpr (Odd.mul ?_ h))) _
-    decide
-
-theorem pentagonal_nonneg (k : ℤ) : 0 ≤ k * (3 * k - 1) / 2 := by
-  suffices 0 ≤ 2 * (k * (3 * k - 1) / 2) by simpa
-  rw [two_pentagonal]
-  obtain h | h := lt_or_ge 0 k
-  · exact mul_nonneg h.le (by linarith)
-  · exact mul_nonneg_of_nonpos_of_nonpos h (by linarith)
-
-theorem two_pentagonal_inj {x y : ℤ} (h : x * (3 * x - 1) = y * (3 * y - 1)) : x = y := by
-  simp_rw [mul_sub_one] at h
-  rw [sub_eq_sub_iff_sub_eq_sub, mul_left_comm x, mul_left_comm y, ← mul_sub] at h
-  rw [mul_self_sub_mul_self, ← mul_assoc, ← sub_eq_zero, ← sub_one_mul, mul_eq_zero] at h
-  obtain h | h := h
-  · simp [← Int.eq_of_mul_eq_one <| eq_of_sub_eq_zero h] at h
-  · exact eq_of_sub_eq_zero h
-
-theorem pentagonal_injective : Function.Injective (fun (k : ℤ) ↦ k * (3 * k - 1) / 2) := by
-  intro a b h
-  have : a * (3 * a - 1) = b * (3 * b - 1) := by
-    rw [← two_pentagonal a, ← two_pentagonal b]
-    simp [h]
-  exact two_pentagonal_inj this
-
-theorem toNat_pentagonal_injective :
-    Function.Injective (fun (k : ℤ) ↦ (k * (3 * k - 1) / 2).toNat) := by
-  intro a b h
-  apply pentagonal_injective
-  zify at h
-  simpa [pentagonal_nonneg] using h
-
-theorem toNat_pentagonal_inj {x y : ℤ}
-    (h : (x * (3 * x - 1) / 2).toNat = (y * (3 * y - 1) / 2).toNat) : x = y := by
-  apply toNat_pentagonal_injective.eq_iff.mp h
-
-end PublicPentagonalNumber
-
 open Filter PowerSeries WithPiTopology
 variable (R : Type*) [CommRing R]
 
 namespace Pentagonal
 
-set_option backward.isDefEq.respectTransparency false in
 theorem tendsto_order_powMulProdOneSubPow_X (k : ℕ) :
     Tendsto (fun i ↦ (powMulProdOneSubPow k i (X : R⟦X⟧)).order) atTop (nhds ⊤) := by
   nontriviality R using Subsingleton.eq_zero
@@ -100,7 +57,6 @@ theorem tendsto_order_powMulProdOneSubPow_X (k : ℕ) :
   norm_cast
   grind
 
-set_option backward.isDefEq.respectTransparency false in
 theorem tendsto_order_neg_X_pow (k : ℕ) :
     Tendsto (fun i ↦ (-(X : R⟦X⟧) ^ (i + k + 1)).order) atTop (nhds ⊤) := by
   nontriviality R using Subsingleton.eq_zero
@@ -110,18 +66,19 @@ theorem tendsto_order_neg_X_pow (k : ℕ) :
   norm_cast
   linarith
 
-set_option backward.isDefEq.respectTransparency false in
 theorem tendsto_order_pow_pentagonal_sub :
-    Tendsto (fun i ↦ ((-1) ^ i * ((X : R⟦X⟧) ^ (i * (3 * i + 1) / 2) -
-      X ^ ((i + 1) * (3 * i + 2) / 2))).order) atTop (nhds ⊤) := by
+    Tendsto (fun (i : ℕ) ↦ ((-1) ^ i * ((X : R⟦X⟧) ^ pentagonal (-i) -
+      X ^ (pentagonal (i + 1)))).order) atTop (nhds ⊤) := by
   nontriviality R using Subsingleton.eq_zero
   refine ENat.tendsto_nhds_top_iff_natCast_lt.mpr fun n ↦ eventually_atTop.mpr ⟨n + 1, ?_⟩
   intro k hk
   rw [sub_eq_add_neg]
   grw [← le_order_mul, ← min_order_le_order_add, order_neg, order_X_pow, order_X_pow]
   apply lt_add_of_nonneg_of_lt (by simp) ?_
-  rw [min_eq_left (by gcongr <;> simp)]
-  rw [Nat.cast_lt, ← Nat.add_one_le_iff, Nat.le_div_iff_mul_le (by simp)]
+  rw [min_eq_left (by simpa using (pentagonal_neg_lt_pentagonal_add_one (Int.natCast_nonneg k)).le)]
+  rw [pentagonal_neg]
+  norm_cast
+  rw [Int.toNat_natCast, ← Nat.add_one_le_iff, Nat.le_div_iff_mul_le (by simp)]
   exact Nat.mul_le_mul hk (by linarith)
 
 end Pentagonal
@@ -145,7 +102,7 @@ namespace WithPiTopology
 variable [TopologicalSpace R]
 
 theorem summable_pow_pentagonal_sub : Summable fun (k : ℕ) ↦
-    ((-1) ^ k * (X ^ (k * (3 * k + 1) / 2) - X ^ ((k + 1) * (3 * k + 2) / 2)) : R⟦X⟧) :=
+    ((-1) ^ k * (X ^ pentagonal (-k) - X ^ pentagonal (k + 1)) : R⟦X⟧) :=
   summable_of_tendsto_order_atTop_nhds_top R (Pentagonal.tendsto_order_pow_pentagonal_sub R)
 
 set_option backward.isDefEq.respectTransparency false in
@@ -155,7 +112,7 @@ $$ \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⟧) =
-    ∑' k, (-1) ^ k * (X ^ (k * (3 * k + 1) / 2) - X ^ ((k + 1) * (3 * k + 2) / 2)) := by
+    ∑' (k : ℕ), (-1) ^ k * (X ^ pentagonal (-k) - X ^ pentagonal (k + 1)) := by
   nontriviality R
   refine Pentagonal.tprod_one_sub_pow ?_ ?_ ?_ ?_ ?_
   · rw [IsTopologicallyNilpotent, tendsto_iff_coeff_tendsto]
@@ -173,9 +130,8 @@ theorem tprod_one_sub_X_pow_eq_tsum_nat [IsTopologicalRing R] [T2Space R] :
     rw [order_X_pow, Nat.cast_lt, ← Nat.add_one_le_iff, Nat.le_div_iff_mul_le (by simp)]
     apply Nat.mul_le_mul <;> linarith
 
-set_option backward.isDefEq.respectTransparency false in
 theorem summable_pow_pentagonal' [IsTopologicalRing R] :
-    Summable fun k ↦ (Int.negOnePow k : R⟦X⟧) * X ^ (k * (3 * k + 1) / 2).toNat := by
+    Summable fun k ↦ (Int.negOnePow k : R⟦X⟧) * X ^ pentagonal (-k) := by
   nontriviality R
   apply Summable.of_add_one_of_neg_add_one
   all_goals
@@ -184,18 +140,18 @@ theorem summable_pow_pentagonal' [IsTopologicalRing R] :
   intro k hk
   grw [← le_order_mul, order_X_pow]
   refine lt_add_of_nonneg_of_lt (by simp) ?_
+  rw [pentagonal_def]
   norm_cast
   grind
 
-set_option backward.isDefEq.respectTransparency false in
 /-- **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.
 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} $$ -/
 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
+    ∏' n, (1 - X ^ (n + 1)) = ∑' k, (Int.negOnePow k : R⟦X⟧) * X ^ pentagonal (-k) := by
   rw [← tsum_nat_add_neg_add_one (summable_pow_pentagonal' R), tprod_one_sub_X_pow_eq_tsum_nat]
   refine tsum_congr fun k ↦ ?_
   rw [sub_eq_add_neg _ (X ^ _), mul_add, ← neg_mul_comm]
@@ -204,47 +160,41 @@ theorem tprod_one_sub_X_pow' [IsTopologicalRing R] [T2Space R] :
   · ring
   · norm_cast
 
-set_option backward.isDefEq.respectTransparency false in
 theorem summable_pow_pentagonal [IsTopologicalRing R] :
-    Summable fun k ↦ (Int.negOnePow k : R⟦X⟧) * X ^ (k * (3 * k - 1) / 2).toNat := by
+    Summable fun k ↦ (Int.negOnePow k : R⟦X⟧) * X ^ pentagonal k := by
   rw [← neg_injective.summable_iff (fun x hx ↦ by absurd hx; use -x; simp)]
   convert summable_pow_pentagonal' R
   rw [Function.comp_apply]
-  exact congr($(by simp) * X ^ (Int.toNat ($(by ring_nf) / 2)))
+  congrm $(by simp) * X ^ _
 
-set_option backward.isDefEq.respectTransparency false in
 /-- **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} $$ -/
 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
+    ∏' n, (1 - X ^ (n + 1)) = ∑' k, (Int.negOnePow k : R⟦X⟧) * X ^ pentagonal k := by
   rw [tprod_one_sub_X_pow', ← neg_injective.tsum_eq (by simp)]
-  exact tsum_congr fun k ↦ congr($(by simp) * X ^ (Int.toNat ($(by ring_nf) / 2)))
+  congrm ∑' k, $(by simp) * X ^ pentagonal $(by simp)
 
 end WithPiTopology
 
 open WithPiTopology
 
-set_option backward.isDefEq.respectTransparency false in
 theorem coeff_prod_one_sub_X_eventually_eq_negOnePow (k : ℤ) :
-    ∀ᶠ s in atTop, (∏ n ∈ s, (1 - X ^ (n + 1) : R⟦X⟧)).coeff (k * (3 * k - 1) / 2).toNat =
-    Int.negOnePow k := by
+    ∀ᶠ s in atTop, (∏ n ∈ s, (1 - X ^ (n + 1) : R⟦X⟧)).coeff (pentagonal k) = Int.negOnePow k := by
   let _ : TopologicalSpace R := ⊥
   have _ : DiscreteTopology R := ⟨rfl⟩
   obtain h := (multipliable_one_sub_X_pow R).hasProd
   rw [tprod_one_sub_X_pow R, HasProd, tendsto_iff_coeff_tendsto] at h
-  specialize h (k * (3 * k - 1) / 2).toNat
+  specialize h (pentagonal k)
   rw [(summable_pow_pentagonal R).map_tsum _ (WithPiTopology.continuous_coeff _ _),
     SummationFilter.unconditional_filter, nhds_discrete, tendsto_pure] at h
   have hpow (i : ℤ) : (i.negOnePow : R⟦X⟧) = C (i.negOnePow : R) := by simp
   simp_rw [hpow, coeff_C_mul, coeff_X_pow] at h
-  rw [tsum_eq_single k fun i hi ↦ by simp [toNat_pentagonal_injective.eq_iff.ne.mpr hi.symm]] at h
+  rw [tsum_eq_single k fun i hi ↦ by simp [hi.symm]] at h
   simpa using h
 
-set_option backward.isDefEq.respectTransparency false in
-theorem coeff_prod_one_sub_X_eventually_eq_zero {n : ℕ}
-    (hn : ∀ k : ℤ, n ≠ (k * (3 * k - 1) / 2).toNat) :
+theorem coeff_prod_one_sub_X_eventually_eq_zero {n : ℕ} (hn : ∀ k : ℤ, n ≠ pentagonal k) :
     ∀ᶠ s in atTop, (∏ n ∈ s, (1 - X ^ (n + 1) : R⟦X⟧)).coeff n = 0 := by
   let _ : TopologicalSpace R := ⊥
   have _ : DiscreteTopology R := ⟨rfl⟩

Mathlib/Topology/Algebra/InfiniteSum/Pentagonal.lean

@@ -5,6 +5,7 @@ Authors: Weiyi Wang
 -/
 module
 
+public import Mathlib.Combinatorics.Enumerative.Pentagonal
 public import Mathlib.Topology.Algebra.InfiniteSum.Ring
 public import Mathlib.Topology.Algebra.TopologicallyNilpotent
 
@@ -49,7 +50,6 @@ $$ b_{k, n} = x^{(k+1)n} (x^{2k + n + 3} - 1) \prod_{i=0}^{n-1} (1 - x^{k + i +
 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))
 
-set_option backward.isDefEq.respectTransparency false in
 /-- `powMulProdOneSubPow` and `aux` have relation
 
 $$ a_{k,n} + x^{3k + 5}a_{k + 1, n} = b_{k, n+1} - b_{k, n} $$ -/
@@ -108,7 +108,6 @@ theorem tprod_one_sub_pow_eq_powMulProdOneSubPow_zero {x : R}
       ← pow_add x 1 1, one_add_one_eq_two, mul_assoc (x ^ 2)]
   simp [hsum.tsum_mul_left, powMulProdOneSubPow]
 
-set_option backward.isDefEq.respectTransparency false in
 /-- Applying the recurrence formula repeatedly, we get
 
 $$ \prod_{n = 0}^{\infty} (1 - x^{n + 1}) =
@@ -146,17 +145,19 @@ public theorem tprod_one_sub_pow {x : R} (hx : IsTopologicallyNilpotent x)
     (hsum : ∀ k, Summable (powMulProdOneSubPow k · x))
     (hlhs : ∀ k, Multipliable (fun n ↦ 1 - x ^ (n + k + 1)))
     (hrhs : Summable fun (k : ℕ) ↦
-      (-1) ^ k * (x ^ (k * (3 * k + 1) / 2) - x ^ ((k + 1) * (3 * k + 2) / 2)))
+      (-1) ^ k * (x ^ pentagonal (-k) - x ^ pentagonal (k + 1)))
     (htail : Tendsto (fun k ↦ (-1) ^ (k + 1) * x ^ ((k + 1) * (3 * k + 4) / 2) *
       ∑' (n : ℕ), powMulProdOneSubPow k n x) atTop (nhds 0)) :
     ∏' n, (1 - x ^ (n + 1)) =
-    ∑' k, (-1) ^ k * (x ^ (k * (3 * k + 1) / 2) - x ^ ((k + 1) * (3 * k + 2) / 2)) := by
+    ∑' (k : ℕ), (-1) ^ k * (x ^ pentagonal (-k) - x ^ pentagonal (k + 1)) := by
   obtain h := fun n ↦ tprod_one_sub_pow_eq_powMulProdOneSubPow n hx hsum hlhs
   simp_rw [← sub_eq_iff_eq_add] at h
   refine (HasSum.tsum_eq ?_).symm
   rw [hrhs.hasSum_iff_tendsto_nat, (map_add_atTop_eq_nat 1).symm]
   apply tendsto_map'
-  simp_rw [Function.comp_def, ← h]
+  have h1 (k : ℕ) : pentagonal (k + 1) = ((k + 1) * (3 * k + 2) / 2) := by grind [pentagonal_def]
+  have h2 (k : ℕ) : pentagonal (-k) = (k * (3 * k + 1) / 2) := by grind [pentagonal_neg]
+  simp_rw [h1, h2, Function.comp_def, ← h]
   rw [← tendsto_sub_nhds_zero_iff]
   simpa using htail.neg