feat: superFactorial_dvd_vandermonde_det (#6893)

mo271 · mo271 · commit 9efe273d66c5 · 2023-11-08T11:24:51.000Z
- [x] depends on: #6806 - [x] depends on: #6812 - [x] depends on: #6918 - [x] depends on: #6927 - [x] depends on: #6929 Co-authored-by: Moritz Firsching <firsching@google.com>
diff --git a/Mathlib/Data/Nat/Factorial/SuperFactorial.lean b/Mathlib/Data/Nat/Factorial/SuperFactorial.lean
@@ -5,13 +5,15 @@ Authors: Moritz Firsching
 -/
 import Mathlib.Algebra.BigOperators.Intervals
 import Mathlib.Data.Nat.Factorial.Basic
+import Mathlib.Data.Polynomial.Monic
 import Mathlib.LinearAlgebra.Vandermonde
+import Mathlib.RingTheory.Polynomial.Pochhammer
 
 /-!
 # Superfactorial
 
 This file defines the [superfactorial](https://en.wikipedia.org/wiki/Superfactorial)
-`sf n = 1! * 2! * 3! * ...* n!`.
+`sf n = 1! * 2! * 3! * ... * n!`.
 
 ## Main declarations
 
@@ -64,6 +66,12 @@ theorem prod_range_factorial_succ : ∀ n : ℕ, ∏ x in range n, (x + 1)! = sf
   | n + 1 => by
     rw [Finset.prod_range_succ, prod_range_factorial_succ n, superFactorial, mul_comm, factorial]
 
+@[simp]
+theorem prod_range_succ_factorial : ∀ n : ℕ, ∏ x in range (n + 1), x ! = sf n
+  | 0 => rfl
+  | n + 1 => by
+    rw [prod_range_succ, prod_range_succ_factorial n, mul_comm, superFactorial]
+
 variable {R : Type*} [CommRing R]
 
 theorem det_vandermonde_id_eq_superFactorial (n : ℕ) :
@@ -79,6 +87,29 @@ theorem det_vandermonde_id_eq_superFactorial (n : ℕ) :
     · rw [Matrix.det_vandermonde] at hn
       simp [hn]
 
+private theorem matrixOf_eval_descPochhammer_eq_mul_matrixOf_choose {n : ℕ} (v : Fin n → ℕ) :
+    (Matrix.of (fun (i j : Fin n) => (descPochhammer ℤ j).eval (v i : ℤ))).det =
+    (∏ i : Fin n, Nat.factorial i) *
+      (Matrix.of (fun (i j : Fin n) => (Nat.choose (v i) (j : ℕ) : ℤ))).det := by
+  convert Matrix.det_mul_row (fun (i : Fin n) => ((Nat.factorial (i : ℕ)):ℤ)) _
+  · rw [Matrix.of_apply, descPochhammer_int_eq_descFactorial _ _]
+    congr
+    exact Nat.descFactorial_eq_factorial_mul_choose _ _
+  · rw [Nat.cast_prod]
+
+theorem superFactorial_dvd_vandermonde_det {n : ℕ} (v : Fin (n + 1) → ℤ) :
+    ↑(Nat.superFactorial n) ∣ (Matrix.vandermonde v).det := by
+  let m := inf' univ ⟨0, mem_univ _⟩ v
+  let w' := fun i ↦ (v i - m).toNat
+  have hw' : ∀ i, (w' i : ℤ) = v i - m := fun i ↦ Int.toNat_sub_of_le (inf'_le _ (mem_univ _))
+  have h :=  Matrix.det_eval_matrixOfPolynomials_eq_det_vandermonde (fun i ↦ ↑(w' i))
+      (fun i => descPochhammer ℤ i)
+      (fun i => descPochhammer_natDegree ℤ i)
+      (fun i => monic_descPochhammer ℤ i)
+  conv_lhs at h => simp only [hw', Matrix.det_vandermonde_sub]
+  use (Matrix.of (fun (i j : Fin (n + 1)) => (Nat.choose (w' i) (j : ℕ) : ℤ))).det
+  simp [h, matrixOf_eval_descPochhammer_eq_mul_matrixOf_choose w', Fin.prod_univ_eq_prod_range]
+
 end SuperFactorial
 
 end Nat
diff --git a/Mathlib/LinearAlgebra/Matrix/Block.lean b/Mathlib/LinearAlgebra/Matrix/Block.lean
@@ -269,6 +269,22 @@ theorem det_of_lowerTriangular [LinearOrder m] (M : Matrix m m R) (h : M.BlockTr
   exact det_of_upperTriangular h.transpose
 #align matrix.det_of_lower_triangular Matrix.det_of_lowerTriangular
 
+open Polynomial
+
+theorem matrixOfPolynomials_blockTriangular {n : ℕ} (p : Fin n → R[X])
+    (h_deg : ∀ i, (p i).natDegree ≤ i) :
+    Matrix.BlockTriangular (Matrix.of (fun (i j : Fin n) => (p j).coeff i)) id :=
+  fun _ j h => by
+    exact coeff_eq_zero_of_natDegree_lt <| Nat.lt_of_le_of_lt (h_deg j) h
+
+theorem det_matrixOfPolynomials {n : ℕ} (p : Fin n → R[X])
+    (h_deg : ∀ i, (p i).natDegree = i) (h_monic : ∀ i, Monic <| p i) :
+    (Matrix.of (fun (i j : Fin n) => (p j).coeff i)).det = 1 := by
+  rw [Matrix.det_of_upperTriangular (Matrix.matrixOfPolynomials_blockTriangular p (fun i ↦
+      Nat.le_of_eq (h_deg i)))]
+  convert prod_const_one with x _
+  rw [Matrix.of_apply, ← h_deg, coeff_natDegree, (h_monic x).leadingCoeff]
+
 /-! ### Invertible -/
 
 
diff --git a/Mathlib/LinearAlgebra/Vandermonde.lean b/Mathlib/LinearAlgebra/Vandermonde.lean
@@ -5,6 +5,7 @@ Authors: Anne Baanen
 -/
 import Mathlib.Algebra.BigOperators.Fin
 import Mathlib.Algebra.GeomSum
+import Mathlib.LinearAlgebra.Matrix.Block
 import Mathlib.LinearAlgebra.Matrix.Determinant
 import Mathlib.LinearAlgebra.Matrix.Nondegenerate
 
@@ -185,4 +186,26 @@ theorem eq_zero_of_forall_pow_sum_mul_pow_eq_zero {R : Type*} [CommRing R] [IsDo
   eq_zero_of_vecMul_eq_zero (det_vandermonde_ne_zero_iff.mpr hf) (funext hfv)
 #align matrix.eq_zero_of_forall_pow_sum_mul_pow_eq_zero Matrix.eq_zero_of_forall_pow_sum_mul_pow_eq_zero
 
+open Polynomial
+
+theorem eval_matrixOfPolynomials_eq_vandermonde_mul_matrixOfPolynomials {n : ℕ}
+    (v : Fin n → R) (p : Fin n → R[X]) (h_deg : ∀ i, (p i).natDegree ≤ i) :
+    Matrix.of (fun i j => ((p j).eval (v i))) =
+    (Matrix.vandermonde v) * (Matrix.of (fun (i j : Fin n) => (p j).coeff i)) := by
+  ext i j
+  rw [Matrix.mul_apply, eval, Matrix.of_apply, eval₂]
+  simp only [eq_intCast, Int.cast_id, Matrix.vandermonde]
+  have : (p j).support ⊆ range n := supp_subset_range <| Nat.lt_of_le_of_lt (h_deg j) <| Fin.prop j
+  rw [sum_eq_of_subset _ (fun j => zero_mul ((v i) ^ j)) this, ← Fin.sum_univ_eq_sum_range]
+  congr
+  ext k
+  rw [mul_comm, Matrix.of_apply, RingHom.id_apply]
+
+theorem det_eval_matrixOfPolynomials_eq_det_vandermonde {n : ℕ} (v : Fin n → R) (p : Fin n → R[X])
+    (h_deg : ∀ i, (p i).natDegree = i) (h_monic : ∀ i, Monic <| p i) :
+    (Matrix.vandermonde v).det = (Matrix.of (fun i j => ((p j).eval (v i)))).det := by
+  rw [Matrix.eval_matrixOfPolynomials_eq_vandermonde_mul_matrixOfPolynomials v p (fun i ↦
+      Nat.le_of_eq (h_deg i)), Matrix.det_mul,
+      Matrix.det_matrixOfPolynomials p h_deg h_monic, mul_one]
+
 end Matrix
diff --git a/docs/references.bib b/docs/references.bib
@@ -595,6 +595,19 @@ @Book{            cassels1967algebraic
   mrclass       = {00.04 (10.00)}
 }
 
+@Article{         chapman1996,
+  author        = {Chapman, Robin},
+  title         = {A Polynomial Taking Integer Values},
+  journal       = {Math. Mag.},
+  fjournal      = {Mathematics Magazine},
+  volume        = {69},
+  year          = {1996},
+  pages         = {121--121},
+  number        = {2},
+  publisher     = {Taylor & Francis, Ltd. on behalf of the Mathematical
+                  Association of America}
+}
+
 @InProceedings{   Chou1994,
   author        = {Chou, Ching-Tsun},
   booktitle     = {Higher Order Logic Theorem Proving and Its Applications},
