Affine Subdivision Determinant

noncomputable def NRR.AffineSubdivisionDeterminant.stepVertexMatrix (n : ℕ) (pi : Equiv.Perm (Fin (n + 1))) : Matrix (Fin (n + 1)) (Fin (n + 1)) ℝ

Matrix whose columns are the vertices of one barycentric subdivision simplex.

Equations

• NRR.AffineSubdivisionDeterminant.stepVertexMatrix n pi r k = ↑(SphereOddDegree.AffineBarycentricSubdivision.prefixBarycenter n pi k) r

noncomputable def NRR.AffineSubdivisionDeterminant.prefixAverageMatrix (n : ℕ) : Matrix (Fin (n + 1)) (Fin (n + 1)) ℝ

Lower triangular prefix-average matrix before permutation of coordinates.

Equations

• NRR.AffineSubdivisionDeterminant.prefixAverageMatrix n r k = if ↑r ≤ ↑k then (↑↑k + 1)⁻¹ else 0

theorem NRR.AffineSubdivisionDeterminant.stepVertexMatrix_eq (n : ℕ) (pi : Equiv.Perm (Fin (n + 1))) : stepVertexMatrix n pi = Equiv.Perm.permMatrix ℝ (Equiv.symm pi) * prefixAverageMatrix n

Factorization of a one-step vertex matrix.

theorem NRR.AffineSubdivisionDeterminant.det_prefixAverageMatrix (n : ℕ) : (prefixAverageMatrix n).det = ∏ k : Fin (n + 1), (↑↑k + 1)⁻¹

Determinant of the prefix-average matrix.

theorem NRR.AffineSubdivisionDeterminant.det_stepVertexMatrix_ne_zero (n : ℕ) (pi : Equiv.Perm (Fin (n + 1))) : (stepVertexMatrix n pi).det ≠ 0

One barycentric subdivision simplex is nondegenerate.

noncomputable def NRR.AffineSubdivisionDeterminant.iterVertexMatrix (n N : ℕ) (rho : Fin N → Equiv.Perm (Fin (n + 1))) : Matrix (Fin (n + 1)) (Fin (n + 1)) ℝ

Vertex matrix of an iterated affine subdivision simplex.

Equations

• NRR.AffineSubdivisionDeterminant.iterVertexMatrix n N rho r k = ↑((SphereOddDegree.AffineBarycentricSubdivision.affineCompMap n N rho) (SphereOddDegree.FiniteSimplex.vertex k)) r

@[simp]

theorem NRR.AffineSubdivisionDeterminant.iterVertexMatrix_zero (n : ℕ) (rho : Fin 0 → Equiv.Perm (Fin (n + 1))) : iterVertexMatrix n 0 rho = 1

theorem NRR.AffineSubdivisionDeterminant.iterVertexMatrix_succ (n N : ℕ) (rho : Fin (N + 1) → Equiv.Perm (Fin (n + 1))) : iterVertexMatrix n (N + 1) rho = (iterVertexMatrix n N fun (i : Fin N) => rho i.castSucc) * stepVertexMatrix n (rho (Fin.last N))

Appending one subdivision step multiplies vertex matrices.

theorem NRR.AffineSubdivisionDeterminant.det_iterVertexMatrix_ne_zero (n N : ℕ) (rho : Fin N → Equiv.Perm (Fin (n + 1))) : (iterVertexMatrix n N rho).det ≠ 0

Every iterated subdivision simplex is nondegenerate.