Mathlib.LinearAlgebra
Linear-algebra helpers staged for Mathlib: monomial-matrix and generalized-permutation lemmas used by causal-discovery identification proofs.
Cholesky 3 core · 7 supporting This file proves that every real symmetric positive-definite matrix factors as the product of the transpose of an upper-triangular matrix with positive diagonal and that matrix itself, and that this factorization is uniq ★ cholesky_exists★ cholesky_unique
Real Cholesky factorization: existence and uniqueness
This file proves that every real symmetric positive-definite matrix factors as the product of the
transpose of an upper-triangular matrix with positive diagonal and that matrix itself, and that
this factorization is unique. Concretely, for a positive-definite matrix M there is a unique
upper-triangular matrix U with strictly positive diagonal entries such that M equals the
transpose of U times U.
The public API consists of the predicate IsUpperTri, the existence theorem
cholesky_exists, and the uniqueness theorem cholesky_unique; the LDL and orthogonal
triangular lemmas expose the proof ingredients needed by those results. Existence is
obtained from the LDL decomposition by absorbing the square roots of the diagonal factor;
uniqueness reduces to orthogonal_upperTri_pos_diag_eq_one, the fact that an orthogonal
upper-triangular matrix with positive diagonal is the identity.
def IsUpperTri reviewed
⚑ flagged
Causalean.Mathlib.LinearAlgebra
For a matrix whose rows and columns are indexed by an ordered set, the upper-triangularity property holds precisely when every entry in a row strictly below its column is zero.
theorem cholesky_exists reviewed
⚑ flagged
Causalean.Mathlib.LinearAlgebra
For a real positive-definite d × d matrix M, there exists an upper-triangular matrix U (zero below the diagonal) with strictly positive diagonal entries such that M factors as Uᵀ · U.
Formal statement
Proof (Lean source)
theorem cholesky_exists (hM : M.PosDef) :
∃ U : Matrix (Fin d) (Fin d) ℝ,
(∀ i j, j < i → U i j = 0) ∧ (∀ i, 0 < U i i) ∧ M = U.transpose * U := by
classical
set s : Fin d → ℝ := fun i => sqrt (diagEntries hM i) with hs
set Dsqrt : Matrix (Fin d) (Fin d) ℝ := diagonal s with hDsqrt
refine ⟨Dsqrt * (lower hM)ᵀ, ?_, ?_, ?_⟩
· -- upper triangular
have hd : Dsqrt.BlockTriangular id := blockTriangular_diagonal s
have hL : ((lower hM)ᵀ).BlockTriangular id := (ldl_lower_blockTriangular hM).transpose
exact (hd.mul hL)
· -- positive diagonal
intro i
rw [Matrix.mul_apply]
rw [Finset.sum_eq_single i]
· simp only [hDsqrt, Matrix.diagonal_apply_eq, Matrix.transpose_apply, ldl_lower_diag_one hM i,
mul_one, hs]
exact Real.sqrt_pos.mpr (ldl_diagEntries_pos hM i)
· intro k _ hki
rw [hDsqrt, Matrix.diagonal_apply_ne' s hki, zero_mul]
· intro h; exact absurd (Finset.mem_univ i) h
· -- M = Uᵀ U
have hLH : (lower hM)ᴴ = (lower hM)ᵀ :=
Matrix.conjTranspose_eq_transpose_of_trivial _
have hDD : Dsqrt * Dsqrt = LDL.diag hM := by
rw [hDsqrt, diagonal_mul_diagonal]
rw [LDL.diag]
congr 1
ext i
simp only [hs, Real.mul_self_sqrt (le_of_lt (ldl_diagEntries_pos hM i))]
have hkey := LDL.lower_conj_diag hM
rw [hLH] at hkey
rw [Matrix.transpose_mul, Matrix.transpose_transpose, Matrix.diagonal_transpose]
rw [← hDsqrt, Matrix.mul_assoc (lower hM) Dsqrt, ← Matrix.mul_assoc Dsqrt Dsqrt, hDD,
← Matrix.mul_assoc]
exact hkey.symm
theorem cholesky_unique reviewed
⚑ flagged
Causalean.Mathlib.LinearAlgebra
For a linearly ordered finite index type ι and a linearly ordered field K, and two matrices U, V indexed by ι × ι and valued in K, if U is upper-triangular, i.e. zero below the diagonal, with strictly positive diagonal entries, V is likewise upper-triangular with strictly positive diagonal entries, and U and V have the same Gram matrix, Uᵀ · U = Vᵀ · V, then U equals V.
Formal statement
hypotheses
ι K :
hUu :
∀ i j
if
j < i
then
U i j = 0
hUp :
∀ i, 0 < U i i
hVu :
∀ i j
if
j < i
then
V i j = 0
hVp :
∀ i, 0 < V i i
hGram :
U.transpose * U = V.transpose * V
conclusion
U = V
Proof (Lean source)
theorem cholesky_unique {ι K : Type*} [Fintype ι] [LinearOrder ι]
[Field K] [LinearOrder K] [IsStrictOrderedRing K] {U V : Matrix ι ι K}
(hUu : ∀ i j, j < i → U i j = 0) (hUp : ∀ i, 0 < U i i)
(hVu : ∀ i j, j < i → V i j = 0) (hVp : ∀ i, 0 < V i i)
(hGram : U.transpose * U = V.transpose * V) : U = V := by
classical
have hUu' : U.BlockTriangular id := hUu
have hVu' : V.BlockTriangular id := hVu
-- `U` is invertible (positive diagonal ⟹ positive determinant).
have hUdet : (0 : K) < U.det := by
rw [Matrix.det_of_upperTriangular hUu']; exact Finset.prod_pos (fun i _ => hUp i)
haveI : Invertible U := U.invertibleOfIsUnitDet (isUnit_iff_ne_zero.mpr hUdet.ne')
-- `U⁻¹` is upper-triangular with reciprocal diagonal entries.
have hUinvU : U⁻¹.BlockTriangular id := blockTriangular_inv_of_blockTriangular hUu'
have hUinv_diag : ∀ i, U⁻¹ i i = (U i i)⁻¹ := by
intro i
have hmul : (U⁻¹ * U) i i = 1 := by rw [Matrix.inv_mul_of_invertible]; simp
rw [Matrix.mul_apply, Finset.sum_eq_single i] at hmul
· field_simp [(hUp i).ne'] at hmul ⊢
linarith [hmul]
· intro k _ hki
rcases lt_or_gt_of_ne hki with hk | hk
· rw [hUinvU (by simpa using hk), zero_mul]
· rw [hUu k i hk, mul_zero]
· intro h; exact absurd (Finset.mem_univ i) h
-- The transition matrix `W = V * U⁻¹`.
set W : Matrix ι ι K := V * U⁻¹ with hW
-- `W` is upper-triangular.
have hWupp : ∀ i j, j < i → W i j = 0 := hVu'.mul hUinvU
-- `W` has strictly positive diagonal.
have hWdiag : ∀ i, W i i = V i i * (U i i)⁻¹ := by
intro i
rw [hW, Matrix.mul_apply, Finset.sum_eq_single i]
· rw [hUinv_diag i]
· intro k _ hki
rcases lt_or_gt_of_ne hki with hk | hk
· rw [hVu i k (by simpa using hk), zero_mul]
· rw [hUinvU (by simpa using hk), mul_zero]
· intro h; exact absurd (Finset.mem_univ i) h
have hWpos : ∀ i, 0 < W i i := by
intro i
rw [hWdiag i]
exact mul_pos (hVp i) (inv_pos.mpr (hUp i))
-- `W` is orthogonal: `Wᵀ * W = 1`.
have hMUV : Uᵀ * U = Vᵀ * V := hGram
have hWortho : Wᵀ * W = 1 := by
rw [hW, Matrix.transpose_mul, Matrix.mul_assoc, ← Matrix.mul_assoc Vᵀ V, ← hMUV,
Matrix.mul_assoc Uᵀ, Matrix.mul_inv_of_invertible, Matrix.mul_one,
Matrix.transpose_nonsing_inv, Matrix.inv_mul_of_invertible]
-- Therefore `W = 1`, i.e. `V * U⁻¹ = 1`, i.e. `V = U`.
have hWeq : W = 1 := orthogonal_upperTri_pos_diag_eq_one hWortho hWupp hWpos
rw [hW] at hWeq
have : V = 1 * U := by rw [← hWeq, Matrix.mul_assoc, Matrix.inv_mul_of_invertible, Matrix.mul_one]
rw [this, Matrix.one_mul]
7 supporting declarations (lemmas, instances)
-
isUpperTri_iff_blockTriangulartheorem — The entrywise upper-triangular predicate is exactly Mathlib's block-triangular predicate for the identity order.Proof (Lean source)
theorem isUpperTri_iff_blockTriangular {ι K : Type*} [LT ι] [Zero K] {U : Matrix ι ι K} : IsUpperTri U ↔ U.BlockTriangular id := by rfl -
ldl_lowerInv_diag_onetheorem — The Gram-Schmidt lower-inverse matrix is unitriangular: its diagonal entries are 1.hypothesesconclusionlowerInv hM i i = 1Proof (Lean source)
theorem ldl_lowerInv_diag_one (hM : M.PosDef) (i : Fin d) : lowerInv hM i i = 1 := by letI := (Mᵀ.toNormedAddCommGroup hM.transpose) letI := (Mᵀ.toInnerProductSpace hM.transpose.posSemidef) have key : ∀ (c : Fin d), c < i → InnerProductSpace.gramSchmidt ℝ (⇑(Pi.basisFun ℝ (Fin d))) c i = 0 := by intro c hc have h2 := InnerProductSpace.gramSchmidt_triangular (𝕜 := ℝ) hc (Pi.basisFun ℝ (Fin d)) simpa using h2 rw [lowerInv, InnerProductSpace.gramSchmidt_def] simp only [Pi.sub_apply, Finset.sum_apply, Pi.basisFun_apply, Pi.single_eq_same, sub_eq_self] refine Finset.sum_eq_zero (fun c hc => ?_) rw [Submodule.starProjection_singleton] change _ * InnerProductSpace.gramSchmidt ℝ (⇑(Pi.basisFun ℝ (Fin d))) c i = 0 rw [key c (Finset.mem_Iio.mp hc), mul_zero] -
ldl_diagEntries_postheorem — The diagonal entries of the LDL decomposition of a real positive-definite matrix are strictly positive.hypothesesconclusion0 < diagEntries hM iProof (Lean source)
theorem ldl_diagEntries_pos (hM : M.PosDef) (i : Fin d) : 0 < diagEntries hM i := by have hne : lowerInv hM i ≠ 0 := by intro h have h1 := ldl_lowerInv_diag_one hM i rw [h] at h1 simp at h1 rw [diagEntries] simp only [EuclideanSpace.inner_toLp_toLp, star_trivial] rw [dotProduct_comm] exact hM.dotProduct_mulVec_pos hne -
ldl_lowerInv_blockTriangulartheorem — LDL.lowerInv is lower-triangular in the BlockTriangular toDual sense.hypothesesconclusionProof (Lean source)
theorem ldl_lowerInv_blockTriangular (hM : M.PosDef) : (lowerInv hM).BlockTriangular toDual := by intro i j hij exact LDL.lowerInv_triangular hM (by simpa using hij) -
ldl_lower_blockTriangulartheorem — LDL.lower (the inverse of LDL.lowerInv) is lower-triangular.hypothesesconclusionProof (Lean source)
theorem ldl_lower_blockTriangular (hM : M.PosDef) : (lower hM).BlockTriangular toDual := by rw [lower] exact blockTriangular_inv_of_blockTriangular (ldl_lowerInv_blockTriangular hM) -
ldl_lower_diag_onetheorem — LDL.lower is unitriangular: its diagonal entries are 1.Proof (Lean source)
theorem ldl_lower_diag_one (hM : M.PosDef) (i : Fin d) : lower hM i i = 1 := by have hlow := ldl_lower_blockTriangular hM have hupp := ldl_lowerInv_blockTriangular hM have hmul : lower hM * lowerInv hM = 1 := by rw [lower]; exact Matrix.inv_mul_of_invertible _ have hii : (lower hM * lowerInv hM) i i = 1 := by rw [hmul]; simp rw [Matrix.mul_apply] at hii rw [Finset.sum_eq_single i] at hii · rw [ldl_lowerInv_diag_one hM i, mul_one] at hii; exact hii · intro k _ hki rcases lt_or_gt_of_ne hki with hk | hk · rw [hupp (by simpa using hk), mul_zero] · rw [hlow (by simpa using hk), zero_mul] · intro h; exact absurd (Finset.mem_univ i) h -
orthogonal_upperTri_pos_diag_eq_onetheorem — An orthogonal (Wᵀ * W = 1) upper-triangular matrix with strictly positive diagonal is the identity matrix.hypothesesι K :hortho :Wᵀ * W = 1hupp :∀ i jifj < ithenW i j = 0hpos :∀ i, 0 < W i iconclusionW = 1Proof (Lean source)
theorem orthogonal_upperTri_pos_diag_eq_one {ι K : Type*} [Fintype ι] [LinearOrder ι] [Field K] [LinearOrder K] [IsStrictOrderedRing K] {W : Matrix ι ι K} (hortho : Wᵀ * W = 1) (hupp : ∀ i j, j < i → W i j = 0) (hpos : ∀ i, 0 < W i i) : W = 1 := by classical haveI : Invertible W := invertibleOfLeftInverse _ _ hortho -- `W⁻¹ = Wᵀ` have hinv : W⁻¹ = Wᵀ := Matrix.inv_eq_left_inv hortho have hWupp : W.BlockTriangular id := hupp -- `Wᵀ` is upper-triangular (as `W⁻¹`) and lower-triangular (as a transpose of upper). have hWTupp : (Wᵀ).BlockTriangular id := hinv ▸ blockTriangular_inv_of_blockTriangular hWupp have hWTlow : (Wᵀ).BlockTriangular toDual := hWupp.transpose -- Hence `Wᵀ` is diagonal: off-diagonal entries vanish. have hWTdiag : ∀ i j, i ≠ j → (Wᵀ) i j = 0 := by intro i j hij rcases lt_or_gt_of_ne hij with h | h · exact hWTlow (by simpa using h) · exact hWTupp (by simpa using h) -- The diagonal entries square to one and are positive, hence equal one. ext i j have hsq : ∀ k, W k k * W k k = 1 := by intro k have := congrFun (congrFun hortho k) k rw [Matrix.mul_apply] at this rw [Finset.sum_eq_single k] at this · simpa [Matrix.transpose_apply] using this · intro l _ hlk have hz : (Wᵀ) k l = 0 := hWTdiag k l (Ne.symm hlk) rw [hz, zero_mul] · intro h; exact absurd (Finset.mem_univ k) h have hdiagone : ∀ k, W k k = 1 := by intro k have h1 := hsq k nlinarith [hpos k] rcases eq_or_ne i j with rfl | hne · simp [hdiagone i] · rcases lt_or_gt_of_ne hne with h | h · -- `i < j`: read off `W i j` from the vanishing transpose entry `Wᵀ j i` have : (Wᵀ) j i = 0 := hWTdiag j i (Ne.symm hne) simpa [Matrix.transpose_apply, Matrix.one_apply_ne hne] using this · -- `j < i`: upper-triangularity kills it rw [hupp i j h, Matrix.one_apply_ne (Ne.symm (by simpa using h.ne))]
ConfluentVandermonde 9 core · 18 supporting This file proves nonsingularity of the Hermite evaluation matrix at distinct complex nodes, together with the pinned variant having one simple node and all remaining nodes doubled. ★ det_confluentVandermonde_ne_zero★ det_pinnedConfluentVandermonde_ne_zero
Confluent Vandermonde matrices
This file proves nonsingularity of the Hermite evaluation matrix at distinct complex nodes, together with the pinned variant having one simple node and all remaining nodes doubled.
def doubledExponent reviewed
⚑ flagged
Causalean.Mathlib.LinearAlgebra
Given a nonnegative integer , the doubled exponent assigns exponent to the -th index in the first block of indices and exponent to the -th index in the second block. The first-block assignment and the second-block assignment together define the encoding.
def doubledCoefficientPolynomial reviewed
⚑ flagged
Causalean.Mathlib.LinearAlgebra
Given a nonnegative integer , a semiring of coefficients, and a coefficient vector indexed by two blocks of positions, the doubled coefficient polynomial is the polynomial whose coefficient at each encoded exponent is the corresponding entry of that vector.
Definition (Lean source)
def confluentVandermonde reviewed
⚑ flagged
Causalean.Mathlib.LinearAlgebra
Given a nonnegative integer , a semiring of coefficients, and node values, the confluent Vandermonde matrix is the square matrix with rows indexed by monomial degrees from zero through , value columns at every node, and first-derivative columns at every node.
theorem det_confluentVandermonde_ne_zero reviewed
⚑ flagged
Causalean.Mathlib.LinearAlgebra
For a positive number of nodes n (1 ≤ n), a field K, and pairwise distinct nodes s : Fin n → K, the confluent Vandermonde determinant at s is nonzero.
Formal statement
hypotheses
conclusion
(confluentVandermonde s).det ≠ 0
Proof (Lean source)
theorem det_confluentVandermonde_ne_zero {n : ℕ} {K : Type*} [Field K] (hn : 1 ≤ n)
(s : Fin n → K) (hs : Injective s) :
(confluentVandermonde s).det ≠ 0 := by
let M := confluentVandermonde s
have hmul : Injective M.transpose.mulVec := by
intro u v huv
apply sub_eq_zero.mp
let w := u - v
have hw : M.transpose.mulVec w = 0 := by
funext b
simp only [w, mulVec, dotProduct, Pi.sub_apply, Pi.zero_apply,
mul_sub, Finset.sum_sub_distrib]
exact sub_eq_zero.mpr (congrFun huv b)
apply doubledCoefficientPolynomial_eq_zero_of_eval_derivative hn s hs w
· intro i
have hi := congrFun hw (inl i)
simpa [M, confluentVandermonde, mulVec, dotProduct,
eval_doubledCoefficientPolynomial, mul_comm] using hi
· intro i
have hi := congrFun hw (inr i)
simpa [M, confluentVandermonde, mulVec, dotProduct,
eval_derivative_doubledCoefficientPolynomial, mul_comm, mul_left_comm,
mul_assoc] using hi
have hu : IsUnit M.transpose := Matrix.mulVec_injective_iff_isUnit.mp hmul
have hdet : IsUnit M.transpose.det :=
hu.map (Matrix.detMonoidHom (n := Fin n ⊕ Fin n) (R := K))
simpa [M, Matrix.det_transpose] using hdet.ne_zero
def pinnedExponent reviewed
⚑ flagged
Causalean.Mathlib.LinearAlgebra
Given a nonnegative integer , the pinned exponent assigns exponent to the -th index in its block of simple-node positions and exponent to the -th index in its block of derivative positions. The simple-node assignment and the derivative-position assignment together define the encoding.
def pinnedSucc reviewed
⚑ flagged
Causalean.Mathlib.LinearAlgebra
Given a nonnegative integer and an index , the pinned successor index is the index .
def pinnedCoefficientPolynomial reviewed
⚑ flagged
Causalean.Mathlib.LinearAlgebra
Given a nonnegative integer , a semiring of coefficients, and a coefficient vector indexed by value positions and derivative positions, the pinned coefficient polynomial is the polynomial whose coefficient at each pinned exponent is the corresponding vector entry.
Definition (Lean source)
def pinnedConfluentVandermonde reviewed
⚑ flagged
Causalean.Mathlib.LinearAlgebra
Given a nonnegative integer , a semiring of coefficients, and node values, the pinned confluent Vandermonde matrix records values at all nodes and first derivatives at nodes one through , omitting the derivative at node zero.
Definition (Lean source)
theorem det_pinnedConfluentVandermonde_ne_zero reviewed
⚑ flagged
Causalean.Mathlib.LinearAlgebra
For a positive number of nodes n (1 ≤ n), a field K, and pairwise distinct nodes s : Fin n → K, the pinned confluent Vandermonde determinant at s is nonzero: one node contributes only value evaluation and every other node contributes both value and first-derivative evaluation.
Formal statement
hypotheses
conclusion
(pinnedConfluentVandermonde s).det ≠ 0
Proof (Lean source)
theorem det_pinnedConfluentVandermonde_ne_zero {n : ℕ} {K : Type*} [Field K]
(hn : 1 ≤ n) (s : Fin n → K) (hs : Injective s) :
(pinnedConfluentVandermonde s).det ≠ 0 := by
let M := pinnedConfluentVandermonde s
have hmul : Injective M.transpose.mulVec := by
intro u v huv
apply sub_eq_zero.mp
let w := u - v
have hw : M.transpose.mulVec w = 0 := by
funext b
simp only [w, mulVec, dotProduct, Pi.sub_apply, Pi.zero_apply,
mul_sub, Finset.sum_sub_distrib]
exact sub_eq_zero.mpr (congrFun huv b)
apply pinnedCoefficientPolynomial_eq_zero_of_eval_derivative hn s hs w
· intro i
have hi := congrFun hw (inl i)
simpa [M, pinnedConfluentVandermonde, mulVec, dotProduct,
eval_pinnedCoefficientPolynomial, mul_comm] using hi
· intro i
have hi := congrFun hw (inr i)
simpa [M, pinnedConfluentVandermonde, mulVec, dotProduct,
eval_derivative_pinnedCoefficientPolynomial, mul_comm, mul_left_comm,
mul_assoc] using hi
have hu : IsUnit M.transpose := Matrix.mulVec_injective_iff_isUnit.mp hmul
have hdet : IsUnit M.transpose.det := hu.map
(Matrix.detMonoidHom (n := Fin n ⊕ Fin (n - 1)) (R := K))
simpa [M, Matrix.det_transpose] using hdet.ne_zero
18 supporting declarations (lemmas, instances)
-
doubledExponent_injectivelemma — The doubled exponent encoding is injective.Proof (Lean source)
lemma doubledExponent_injective {n : ℕ} : Injective (doubledExponent : Fin n ⊕ Fin n → ℕ) := by intro i j hij rcases i with i | i <;> rcases j with j | j · simp only [doubledExponent] at hij exact congrArg inl (Fin.ext hij) · simp only [doubledExponent] at hij exfalso have := i.isLt omega · simp only [doubledExponent] at hij exfalso have := j.isLt omega · simp only [doubledExponent] at hij exact congrArg inr (Fin.ext (Nat.add_left_cancel hij)) -
doubledExponent_ltlemma — Every doubled exponent is strictly below 2n.Proof (Lean source)
lemma doubledExponent_lt {n : ℕ} (i : Fin n ⊕ Fin n) : doubledExponent i < 2 * n := by rcases i with i | i <;> simp only [doubledExponent] · omega · have := i.isLt omega -
coeff_doubledCoefficientPolynomiallemma — Reading a doubled coefficient polynomial at an encoded exponent recovers the corresponding coefficient.hypothesesconclusion(doubledCoefficientPolynomial v).coeff (doubledExponent i) = v iProof (Lean source)
lemma coeff_doubledCoefficientPolynomial {n : ℕ} {K : Type*} [Semiring K] (v : Fin n ⊕ Fin n → K) (i : Fin n ⊕ Fin n) : (doubledCoefficientPolynomial v).coeff (doubledExponent i) = v i := by classical change (Polynomial.lcoeff K (doubledExponent i)) (∑ j, Polynomial.monomial (doubledExponent j) (v j)) = v i rw [map_sum] rw [Finset.sum_eq_single i] · simp · intro j _ hji rw [Polynomial.lcoeff_apply, Polynomial.coeff_monomial] exact if_neg (doubledExponent_injective.ne hji) · simp -
doubledCoefficientPolynomial_eq_zero_ifflemma — A doubled coefficient polynomial vanishes exactly when its coefficient vector vanishes.hypothesesconclusiondoubledCoefficientPolynomial v = 0 ↔ v = 0Proof (Lean source)
lemma doubledCoefficientPolynomial_eq_zero_iff {n : ℕ} {K : Type*} [Semiring K] (v : Fin n ⊕ Fin n → K) : doubledCoefficientPolynomial v = 0 ↔ v = 0 := by constructor · intro hp funext i have := congrArg (fun p : Polynomial K => p.coeff (doubledExponent i)) hp simpa [coeff_doubledCoefficientPolynomial] using this · rintro rfl simp [doubledCoefficientPolynomial] -
natDegree_doubledCoefficientPolynomial_ltlemma — A doubled coefficient polynomial has degree below 2n when n is positive.hypothesesconclusion(doubledCoefficientPolynomial v).natDegree < 2 * nProof (Lean source)
lemma natDegree_doubledCoefficientPolynomial_lt {n : ℕ} {K : Type*} [Semiring K] (hn : 1 ≤ n) {v : Fin n ⊕ Fin n → K} : (doubledCoefficientPolynomial v).natDegree < 2 * n := by apply lt_of_le_of_lt (Polynomial.natDegree_sum_le_of_forall_le (univ) _ (fun i _ => (Polynomial.natDegree_monomial_le _).trans (Nat.le_pred_of_lt (doubledExponent_lt i)))) have hpos : 0 < 2 * n := by omega exact Nat.pred_lt hpos.ne' -
eval_doubledCoefficientPolynomiallemma — Evaluating a polynomial whose coefficients are indexed by two blocks of monomial powers gives the finite sum of those coefficients weighted by the corresponding powers of the evaluation point.hypothesesconclusion(doubledCoefficientPolynomial v).eval x = ∑ a, x ^ doubledExponent a * v aProof (Lean source)
lemma eval_doubledCoefficientPolynomial {n : ℕ} {K : Type*} [CommSemiring K] (v : Fin n ⊕ Fin n → K) (x : K) : (doubledCoefficientPolynomial v).eval x = ∑ a, x ^ doubledExponent a * v a := by simp only [doubledCoefficientPolynomial] rw [Polynomial.eval_finset_sum] simp only [Polynomial.eval_monomial] apply Finset.sum_congr rfl intro a _ ring -
eval_derivative_doubledCoefficientPolynomiallemma — Evaluating the derivative of a polynomial whose coefficients are indexed by two blocks of monomial powers gives the finite sum of coefficients weighted by their monomial exponents and the corresponding reduced powers.hypothesesconclusion(doubledCoefficientPolynomial v).derivative.eval x= ∑ a, ((doubledExponent a : K) * x ^ (doubledExponent a - 1)) * v aProof (Lean source)
lemma eval_derivative_doubledCoefficientPolynomial {n : ℕ} {K : Type*} [CommSemiring K] (v : Fin n ⊕ Fin n → K) (x : K) : (doubledCoefficientPolynomial v).derivative.eval x = ∑ a, ((doubledExponent a : K) * x ^ (doubledExponent a - 1)) * v a := by simp only [doubledCoefficientPolynomial, map_sum, Polynomial.derivative_monomial] rw [Polynomial.eval_finset_sum] simp only [Polynomial.eval_monomial] apply Finset.sum_congr rfl intro a _ ring -
doubledCoefficientPolynomial_eq_zero_of_eval_derivativelemma — A polynomial of degree below 2n whose value and derivative vanish at n distinct points is zero.hypothesesn :ℕK :Type*Field Khn :1 ≤ ns :Fin n → Khs :heval :∀ i, (doubledCoefficientPolynomial v).eval (s i) = 0hderiv :∀ i, (doubledCoefficientPolynomial v).derivative.eval (s i) = 0conclusionv = 0Proof (Lean source)
lemma doubledCoefficientPolynomial_eq_zero_of_eval_derivative {n : ℕ} {K : Type*} [Field K] (hn : 1 ≤ n) (s : Fin n → K) (hs : Injective s) (v : Fin n ⊕ Fin n → K) (heval : ∀ i, (doubledCoefficientPolynomial v).eval (s i) = 0) (hderiv : ∀ i, (doubledCoefficientPolynomial v).derivative.eval (s i) = 0) : v = 0 := by by_contra hv have hp : doubledCoefficientPolynomial v ≠ 0 := (doubledCoefficientPolynomial_eq_zero_iff v).not.mpr hv have hfactor (i : Fin n) : (Polynomial.X - Polynomial.C (s i)) ^ 2 ∣ doubledCoefficientPolynomial v := by rw [← Polynomial.le_rootMultiplicity_iff hp] apply (Polynomial.one_lt_rootMultiplicity_iff_isRoot hp).2 exact ⟨heval i, hderiv i⟩ have hcop : Pairwise (Function.onFun IsCoprime fun i : Fin n => (Polynomial.X - Polynomial.C (s i)) ^ 2) := by intro i j hij apply (Polynomial.isCoprime_X_sub_C_of_isUnit_sub (show IsUnit (s i - s j) from (sub_ne_zero.mpr (hs.ne hij)).isUnit)).pow have hprod : (∏ i : Fin n, (Polynomial.X - Polynomial.C (s i)) ^ 2) ∣ doubledCoefficientPolynomial v := Fintype.prod_dvd_of_coprime hcop hfactor have hdegree := Polynomial.natDegree_le_of_dvd hprod hp have hleft : (∏ i : Fin n, (Polynomial.X - Polynomial.C (s i)) ^ 2).natDegree = 2 * n := by calc _ = ∑ i : Fin n, ((Polynomial.X - Polynomial.C (s i)) ^ 2).natDegree := by apply Polynomial.natDegree_prod intro i _ exact pow_ne_zero _ (Polynomial.X_sub_C_ne_zero (s i)) _ = 2 * n := by simp [Polynomial.natDegree_pow, Nat.mul_comm] rw [hleft] at hdegree exact (not_lt_of_ge hdegree) (natDegree_doubledCoefficientPolynomial_lt hn) -
pinnedSucc_injectivelemma — The positive-node embedding is injective.Proof (Lean source)
lemma pinnedSucc_injective {n : ℕ} : Injective (pinnedSucc (n := n)) := by intro i j hij apply Fin.ext have := congrArg val hij simp only [pinnedSucc] at this omega -
pinnedSucc_ne_zerolemma — A positive-node index never equals the distinguished zero node.Proof (Lean source)
lemma pinnedSucc_ne_zero {n : ℕ} (hn : 1 ≤ n) (i : Fin (n - 1)) : pinnedSucc i ≠ ⟨0, hn⟩ := by intro h have := congrArg val h simp [pinnedSucc] at this -
pinnedExponent_injectivelemma — The pinned exponent encoding is injective.Proof (Lean source)
lemma pinnedExponent_injective {n : ℕ} : Injective (pinnedExponent : Fin n ⊕ Fin (n - 1) → ℕ) := by intro i j hij rcases i with i | i <;> rcases j with j | j · exact congrArg inl (Fin.ext hij) · exfalso simp only [pinnedExponent] at hij have := i.isLt omega · exfalso simp only [pinnedExponent] at hij have := j.isLt omega · simp only [pinnedExponent] at hij exact congrArg inr (Fin.ext (Nat.add_left_cancel hij)) -
pinnedExponent_ltlemma — Every pinned exponent is strictly below 2n - 1.Proof (Lean source)
lemma pinnedExponent_lt {n : ℕ} (i : Fin n ⊕ Fin (n - 1)) : pinnedExponent i < 2 * n - 1 := by rcases i with i | i <;> simp only [pinnedExponent] · have := i.isLt omega · have := i.isLt omega -
coeff_pinnedCoefficientPolynomiallemma — Reading a pinned coefficient polynomial at an encoded exponent recovers the corresponding coefficient.hypothesesconclusion(pinnedCoefficientPolynomial v).coeff (pinnedExponent i) = v iProof (Lean source)
lemma coeff_pinnedCoefficientPolynomial {n : ℕ} {K : Type*} [Semiring K] (v : Fin n ⊕ Fin (n - 1) → K) (i : Fin n ⊕ Fin (n - 1)) : (pinnedCoefficientPolynomial v).coeff (pinnedExponent i) = v i := by classical change (Polynomial.lcoeff K (pinnedExponent i)) (∑ j, Polynomial.monomial (pinnedExponent j) (v j)) = v i rw [map_sum, Finset.sum_eq_single i] · simp · intro j _ hji rw [Polynomial.lcoeff_apply, Polynomial.coeff_monomial] exact if_neg (pinnedExponent_injective.ne hji) · simp -
pinnedCoefficientPolynomial_eq_zero_ifflemma — A pinned coefficient polynomial vanishes exactly when its coefficient vector vanishes.hypothesesconclusionpinnedCoefficientPolynomial v = 0 ↔ v = 0Proof (Lean source)
lemma pinnedCoefficientPolynomial_eq_zero_iff {n : ℕ} {K : Type*} [Semiring K] (v : Fin n ⊕ Fin (n - 1) → K) : pinnedCoefficientPolynomial v = 0 ↔ v = 0 := by constructor · intro hp funext i have hi := congrArg (fun p : Polynomial K => p.coeff (pinnedExponent i)) hp simpa [coeff_pinnedCoefficientPolynomial] using hi · rintro rfl simp [pinnedCoefficientPolynomial] -
natDegree_pinnedCoefficientPolynomial_ltlemma — A pinned coefficient polynomial has degree below 2n - 1.hypothesesconclusion(pinnedCoefficientPolynomial v).natDegree < 2 * n - 1Proof (Lean source)
lemma natDegree_pinnedCoefficientPolynomial_lt {n : ℕ} {K : Type*} [Semiring K] (hn : 1 ≤ n) {v : Fin n ⊕ Fin (n - 1) → K} : (pinnedCoefficientPolynomial v).natDegree < 2 * n - 1 := by have hpos : 0 < 2 * n - 1 := by omega apply lt_of_le_of_lt (Polynomial.natDegree_sum_le_of_forall_le (univ) _ (fun i _ => (Polynomial.natDegree_monomial_le _).trans (Nat.le_pred_of_lt (pinnedExponent_lt i)))) exact Nat.pred_lt hpos.ne' -
eval_pinnedCoefficientPolynomiallemma — Evaluating a pinned coefficient polynomial at a point equals the sum of its coefficients, each weighted by that point raised to the coefficient's associated pinned exponent.hypothesesconclusion(pinnedCoefficientPolynomial v).eval x = ∑ a, x ^ pinnedExponent a * v aProof (Lean source)
lemma eval_pinnedCoefficientPolynomial {n : ℕ} {K : Type*} [Field K] (v : Fin n ⊕ Fin (n - 1) → K) (x : K) : (pinnedCoefficientPolynomial v).eval x = ∑ a, x ^ pinnedExponent a * v a := by simp only [pinnedCoefficientPolynomial] rw [Polynomial.eval_finset_sum] simp only [Polynomial.eval_monomial] apply Finset.sum_congr rfl intro a _ ring -
eval_derivative_pinnedCoefficientPolynomiallemma — Evaluating the derivative of a pinned coefficient polynomial at a point equals the sum of its coefficients weighted by the corresponding derivative monomial values at that point.hypothesesconclusion(pinnedCoefficientPolynomial v).derivative.eval x= ∑ a, ((pinnedExponent a : K) * x ^ (pinnedExponent a - 1)) * v aProof (Lean source)
lemma eval_derivative_pinnedCoefficientPolynomial {n : ℕ} {K : Type*} [Field K] (v : Fin n ⊕ Fin (n - 1) → K) (x : K) : (pinnedCoefficientPolynomial v).derivative.eval x = ∑ a, ((pinnedExponent a : K) * x ^ (pinnedExponent a - 1)) * v a := by simp only [pinnedCoefficientPolynomial, map_sum, Polynomial.derivative_monomial] rw [Polynomial.eval_finset_sum] simp only [Polynomial.eval_monomial] apply Finset.sum_congr rfl intro a _ ring -
pinnedCoefficientPolynomial_eq_zero_of_eval_derivativelemma — A polynomial in the pinned coefficient model is zero when it vanishes at all nodes and its derivative vanishes at every nondistinguished node.hypothesesn :ℕK :Type*Field Khn :1 ≤ ns :Fin n → Khs :heval :∀ i, (pinnedCoefficientPolynomial v).eval (s i) = 0hderiv :conclusionv = 0Proof (Lean source)
lemma pinnedCoefficientPolynomial_eq_zero_of_eval_derivative {n : ℕ} {K : Type*} [Field K] (hn : 1 ≤ n) (s : Fin n → K) (hs : Injective s) (v : Fin n ⊕ Fin (n - 1) → K) (heval : ∀ i, (pinnedCoefficientPolynomial v).eval (s i) = 0) (hderiv : ∀ i : Fin (n - 1), (pinnedCoefficientPolynomial v).derivative.eval (s (pinnedSucc i)) = 0) : v = 0 := by by_contra hv have hp : pinnedCoefficientPolynomial v ≠ 0 := (pinnedCoefficientPolynomial_eq_zero_iff v).not.mpr hv let first := Polynomial.X - Polynomial.C (s ⟨0, hn⟩) let rest : Fin (n - 1) → Polynomial K := fun i => (Polynomial.X - Polynomial.C (s (pinnedSucc i))) ^ 2 have hfirst : first ∣ pinnedCoefficientPolynomial v := by rw [Polynomial.dvd_iff_isRoot] exact heval ⟨0, hn⟩ have hrest (i : Fin (n - 1)) : rest i ∣ pinnedCoefficientPolynomial v := by dsimp [rest] rw [← Polynomial.le_rootMultiplicity_iff hp] apply (Polynomial.one_lt_rootMultiplicity_iff_isRoot hp).2 exact ⟨heval (pinnedSucc i), hderiv i⟩ have hrestcop : Pairwise (onFun IsCoprime rest) := by intro i j hij apply (Polynomial.isCoprime_X_sub_C_of_isUnit_sub (show IsUnit (s (pinnedSucc i) - s (pinnedSucc j)) from (sub_ne_zero.mpr (by intro h apply hij apply pinnedSucc_injective exact hs h)).isUnit)).pow have hrestprod : (∏ i, rest i) ∣ pinnedCoefficientPolynomial v := Fintype.prod_dvd_of_coprime hrestcop hrest have hfirstrest : IsCoprime first (∏ i, rest i) := by apply IsCoprime.prod_right intro i _ dsimp [first, rest] exact (Polynomial.isCoprime_X_sub_C_of_isUnit_sub (show IsUnit (s ⟨0, hn⟩ - s (pinnedSucc i)) from (sub_ne_zero.mpr (hs.ne (pinnedSucc_ne_zero hn i).symm)).isUnit)).pow_right have htotal : first * (∏ i, rest i) ∣ pinnedCoefficientPolynomial v := hfirstrest.mul_dvd hfirst hrestprod have hdegree := Polynomial.natDegree_le_of_dvd htotal hp have hleft : (first * ∏ i, rest i).natDegree = 2 * n - 1 := by rw [Polynomial.natDegree_mul (Polynomial.X_sub_C_ne_zero _) (Finset.prod_ne_zero_iff.mpr (fun i _ => pow_ne_zero _ (Polynomial.X_sub_C_ne_zero _)))] have hrestdeg : (∏ i, rest i).natDegree = 2 * (n - 1) := by calc _ = ∑ i : Fin (n - 1), (rest i).natDegree := by apply Polynomial.natDegree_prod intro i _ exact pow_ne_zero _ (Polynomial.X_sub_C_ne_zero _) _ = 2 * (n - 1) := by simp [rest, Polynomial.natDegree_pow, Nat.mul_comm] rw [hrestdeg] simp omega rw [hleft] at hdegree exact (not_lt_of_ge hdegree) (natDegree_pinnedCoefficientPolynomial_lt hn)
MonomialMatrix 3 core · 0 supporting This file collects the linear-algebra facts about generalized-permutation (monomial) matrices that underlie linear causal-discovery identification arguments. ★ genPerm_of_det_ne_zero_of_colSupport★ perm_uniqueness★ eq_of_genPerm_triangular_unitDiag
Generalized-permutation (monomial) matrices
This file collects the linear-algebra facts about generalized-permutation (monomial) matrices that underlie linear causal-discovery identification arguments. A generalized-permutation matrix has exactly one non-zero entry in each row and column — equivalently, it is a permutation composed with a non-zero diagonal rescaling. Such matrices are the ambiguity group of independent component analysis: a mixing matrix is recovered only up to relabelling and rescaling its columns. The three results here are: (1) an invertible matrix with at most one non-zero entry per column is automatically of this generalized-permutation form; (2) a simultaneous row/column permutation of a lower-triangular matrix with non-zero diagonal keeps a non-zero diagonal exactly when the two permutations agree; and (3) two unit-diagonal matrices related by a generalized permutation, one of them triangular in a causal order, must be equal. They are consumed by the LiNGAM and linear-causal-disentanglement developments to turn an ICA-level identification (sharp only up to generalized permutation) into a sharp structural identification.
theorem genPerm_of_det_ne_zero_of_colSupport reviewed
⚑ flagged
Causalean.Mathlib.LinearAlgebra
For a finite index type ι and a commutative ring K, and a square matrix W over ι × ι valued in K with nonzero determinant, if every column of W has at most one non-zero entry (for any two distinct rows i ≠ k, at least one of W i j, W k j vanishes at column j), then W is a generalized permutation matrix: there are a permutation τ of ι and non-zero scalings d with W i j = if j = τ i then d i else 0.
Formal statement
hypotheses
ι K :
hW :
W.det ≠ 0
hcol :
∀ j i k
if
i ≠ k
then
W i j = 0 ∨ W k j = 0
conclusion
∃ (τ : Perm ι) (d : ι → K),
conclusion 1
i :
d i ≠ 0
conclusion 2
i j :
W i j = if j = τ i then d i else 0
Proof (Lean source)
theorem genPerm_of_det_ne_zero_of_colSupport {ι K : Type*} [Fintype ι] [DecidableEq ι]
[CommRing K] {W : Matrix ι ι K} (hW : W.det ≠ 0)
(hcol : ∀ j i k, i ≠ k → W i j = 0 ∨ W k j = 0) :
∃ (τ : Perm ι) (d : ι → K), (∀ i, d i ≠ 0) ∧
∀ i j, W i j = if j = τ i then d i else 0 := by
classical
have hcol_nonzero : ∀ j, ∃ i, W i j ≠ 0 := by
intro j
by_contra hzero
have hcol_zero : ∀ i, W i j = 0 := by
intro i
by_contra hi
exact hzero ⟨i, hi⟩
exact hW (Matrix.det_eq_zero_of_column_eq_zero j hcol_zero)
let ρ : ι → ι := fun j => choose (hcol_nonzero j)
have hρ_ne : ∀ j, W (ρ j) j ≠ 0 := by
intro j
exact Classical.choose_spec (hcol_nonzero j)
have hρ_unique : ∀ j i, W i j ≠ 0 → i = ρ j := by
intro j i hi
by_contra hne
cases hcol j i (ρ j) hne with
| inl h => exact hi h
| inr h => exact hρ_ne j h
have hρ_zero : ∀ j i, i ≠ ρ j → W i j = 0 := by
intro j i hi
by_contra hne
exact hi (hρ_unique j i hne)
have hρ_surj : Surjective ρ := by
by_contra hsurj
have hmissing : ∃ i, ∀ j, ρ j ≠ i := by
simpa [Surjective] using hsurj
obtain ⟨i, hi⟩ := hmissing
have hrow_zero : ∀ j, W i j = 0 := by
intro j
exact hρ_zero j i (fun h => hi j h.symm)
exact hW (Matrix.det_eq_zero_of_row_eq_zero i hrow_zero)
have hρ_inj : Injective ρ := (Finite.injective_iff_surjective).2 hρ_surj
let ρE : Perm ι := Equiv.ofBijective ρ ⟨hρ_inj, hρ_surj⟩
let τ : Perm ι := ρE.symm
let d : ι → K := fun i => W i (τ i)
refine ⟨τ, d, ?_, ?_⟩
· intro i
have hρτ : ρ (τ i) = i := by
change ρE (ρE.symm i) = i
simp
have hne := hρ_ne (τ i)
simpa [d, hρτ] using hne
· intro i j
by_cases hj : j = τ i
· simp [d, hj]
· have hiρ : i ≠ ρ j := by
intro hi
apply hj
calc
j = ρE.symm (ρE j) := by simp
_ = ρE.symm (ρ j) := rfl
_ = ρE.symm i := by rw [← hi]
_ = τ i := rfl
have hzero : W i j = 0 := hρ_zero j i hiρ
simp [hj, hzero]
theorem perm_uniqueness reviewed
⚑ flagged
Causalean.Mathlib.LinearAlgebra
Permutation uniqueness for lower-triangular matrices (LiNGAM Appendix A, Lemma 1). For a matrix M over Fin n × Fin n that is lower-triangular (M i j = 0 whenever i < j) with non-zero diagonal entries, and permutations σ, τ of Fin n, the row/column-permuted matrix (i ↦ M (σ i) (τ i)) has a non-zero diagonal at every i if and only if σ = τ.
Formal statement
Proof (Lean source)
theorem perm_uniqueness {n : ℕ} {K : Type*} [Zero K] {M : Matrix (Fin n) (Fin n) K}
(hLT : ∀ i j, i < j → M i j = 0) (hdiag : ∀ i, M i i ≠ 0)
{σ τ : Perm (Fin n)} :
(∀ i, M (σ i) (τ i) ≠ 0) ↔ σ = τ := by
constructor
· intro h
have hge : ∀ i, (τ i : ℕ) ≤ (σ i : ℕ) := by
intro i
by_contra hlt
push_neg at hlt
exact h i (hLT (σ i) (τ i) (by exact_mod_cast hlt))
have hsum : ∑ i, (σ i : ℕ) = ∑ i, (τ i : ℕ) := by
rw [Equiv.sum_comp σ (fun i => (i : ℕ)), Equiv.sum_comp τ (fun i => (i : ℕ))]
have heq : ∀ i, (σ i : ℕ) = (τ i : ℕ) := by
have hle : ∀ i ∈ univ, (τ i : ℕ) ≤ (σ i : ℕ) := fun i _ => hge i
have := (Finset.sum_eq_sum_iff_of_le hle).1 hsum.symm
intro i; exact ((this i (Finset.mem_univ i)).symm)
exact Equiv.ext fun i => Fin.val_injective (heq i)
· rintro rfl i
exact hdiag (σ i)
theorem eq_of_genPerm_triangular_unitDiag reviewed
⚑ flagged
Causalean.Mathlib.LinearAlgebra
Generalized-permutation reduction. For matrices C, C' over Fin n × Fin n valued in K, if C has unit diagonal and C' has unit diagonal, C is lower triangular in some causal order σ (C i j = 0 when σ i < σ j), and C' is obtained from C by a generalized permutation with permutation τ and scalings d, i.e. C' i j = d i · C (τ i) j for all i, j, then C = C': the unit diagonal plus triangularity force the underlying permutation to be the identity and every scaling to be one. (Formerly Discovery.LiNGAM.lingam_reduction.)
Formal statement
hypotheses
n :
ℕ
K :
hCdiag :
∀ i, C i i = 1
hC'diag :
∀ i, C' i i = 1
hCtri :
∀ i j
if
σ i < σ j
then
C i j = 0
d :
Fin n → K
hW :
∀ i j, C' i j = d i * C (τ i) j
conclusion
C = C'
Proof (Lean source)
theorem eq_of_genPerm_triangular_unitDiag {n : ℕ} {K : Type*}
[MulZeroOneClass K] [Nontrivial K] {C C' : Matrix (Fin n) (Fin n) K}
(hCdiag : ∀ i, C i i = 1) (hC'diag : ∀ i, C' i i = 1)
{σ : Perm (Fin n)} (hCtri : ∀ i j, σ i < σ j → C i j = 0)
{τ : Perm (Fin n)} {d : Fin n → K}
(hW : ∀ i j, C' i j = d i * C (τ i) j) :
C = C' := by
have hne : ∀ i, C (τ i) i ≠ 0 := by
intro i hzero
have h := hW i i
rw [hzero, mul_zero, hC'diag i] at h
exact one_ne_zero h
have hle : ∀ i, (σ i : ℕ) ≤ (σ (τ i) : ℕ) := by
intro i
by_contra h
push_neg at h
exact hne i (hCtri (τ i) i (by exact_mod_cast h))
have hsum : ∑ i, (σ (τ i) : ℕ) = ∑ i, (σ i : ℕ) :=
Equiv.sum_comp τ (fun i => (σ i : ℕ))
have heqσ : ∀ i, (σ (τ i) : ℕ) = (σ i : ℕ) := by
have hle' : ∀ i ∈ univ, (σ i : ℕ) ≤ (σ (τ i) : ℕ) := fun i _ => hle i
exact fun i => ((Finset.sum_eq_sum_iff_of_le hle').1 hsum.symm i (Finset.mem_univ i)).symm
have hτ : ∀ i, τ i = i := fun i => σ.injective (Fin.val_injective (heqσ i))
have hd1 : ∀ i, d i = 1 := by
intro i
have h := hW i i
rw [hτ i, hCdiag i, mul_one, hC'diag i] at h
exact h.symm
ext i j
rw [hW i j, hτ i, hd1 i, one_mul]
StackedVandermonde 4 core · 0 supporting This file gives a constructive injectivity certificate for a stacked family of weighted Vandermonde evaluation maps at distinct nodes in a commutative domain. ★ stacked_contraction_injective_of_generic_weights
Stacked Vandermonde systems
This file gives a constructive injectivity certificate for a stacked family of weighted Vandermonde evaluation maps at distinct nodes in a commutative domain.
def affineBinaryPower reviewed
⚑ flagged
Causalean.Mathlib.LinearAlgebra
Given an element of a multiplicative monoid and a nonnegative integer , the affine power vector is the vector indexed by the integers from zero through whose entry at is .
def stackedContraction reviewed
⚑ flagged
Causalean.Mathlib.LinearAlgebra
Given a nonnegative integer , slope values, a weight assigned to each slope and each of the blocks, and a coefficient attached to each slope, the stacked contraction maps a block index and an exponent to the sum, over all slopes, of the weight times the coefficient times the -th power of that slope.
def blockVandermondeWitnessWeights reviewed
⚑ flagged
Causalean.Mathlib.LinearAlgebra
Given a positive integer , the block-Vandermonde witness weights assign weight one only to index zero in block zero and to every nonzero index in block , and assign weight zero in all other cases. The first block is chosen as block zero, the second as block , and the stated case assignment defines the weights.
Definition (Lean source)
parameters
theorem stacked_contraction_injective_of_generic_weights reviewed
⚑ flagged
Causalean.Mathlib.LinearAlgebra
For a commutative integral domain K, at least three indices N + 1 (2 ≤ N), and pairwise distinct slope values slopes : Fin (N + 1) → K, there exist weights Fin (N + 1) → Fin N → K for which the stacked contraction is injective. The first block detects coordinate 0, while the last block is a square Vandermonde system on coordinates 1,…,N.
Formal statement
Proof (Lean source)
theorem stacked_contraction_injective_of_generic_weights {K : Type*} [CommRing K] [IsDomain K]
{N : ℕ} (hN : 2 ≤ N) (slopes : Fin (N + 1) → K)
(hslopes : Injective slopes) :
∃ weights : Fin (N + 1) → Fin N → K,
Injective (stackedContraction N slopes weights) := by
let zeroBlock : Fin N := ⟨0, by omega⟩
let topBlock : Fin N := ⟨N - 1, sub_lt (by omega) (by omega)⟩
have htop_ne_zero : topBlock ≠ zeroBlock := by
intro h
have : N - 1 = 0 := Fin.ext_iff.mp h
omega
have hzero_ne_top : (0 : ℕ) ≠ N - 1 := by omega
refine ⟨blockVandermondeWitnessWeights N (by omega), ?_⟩
intro e e' he
have hzero : e 0 = e' 0 := by
have h := congrFun (congrFun he zeroBlock) (0 : Fin 1)
simpa [stackedContraction, blockVandermondeWitnessWeights,
affineBinaryPower, zeroBlock, topBlock, htop_ne_zero,
hzero_ne_top, Fin.sum_univ_succ] using h
have hsucc : (fun i : Fin N => e i.succ) = fun i => e' i.succ := by
have htop := fun r => congrFun (congrFun he topBlock) r
have hsum : ∀ r : Fin N,
(∑ i : Fin N, e i.succ * slopes i.succ ^ (r : ℕ)) =
∑ i : Fin N, e' i.succ * slopes i.succ ^ (r : ℕ) := by
intro r
let rTop : Fin (topBlock.1 + 1) := ⟨r.1, by
change r.1 < N - 1 + 1
omega⟩
simpa [stackedContraction, blockVandermondeWitnessWeights,
affineBinaryPower, zeroBlock, topBlock, htop_ne_zero,
Fin.sum_univ_succ, rTop] using htop rTop
have hv : (fun i : Fin N => e i.succ - e' i.succ) = 0 := by
apply Matrix.eq_zero_of_vecMul_eq_zero
(Matrix.det_vandermonde_ne_zero_iff.mpr
(hslopes.comp (Fin.succ_injective N)))
funext r
change ∑ i : Fin N, (e i.succ - e' i.succ) * slopes i.succ ^ (r : ℕ) = 0
calc
∑ i : Fin N, (e i.succ - e' i.succ) * slopes i.succ ^ (r : ℕ) =
(∑ i : Fin N, e i.succ * slopes i.succ ^ (r : ℕ)) -
∑ i : Fin N, e' i.succ * slopes i.succ ^ (r : ℕ) := by
rw [← Finset.sum_sub_distrib]
apply Finset.sum_congr rfl
intro i _
ring
_ = 0 := sub_eq_zero.mpr (hsum r)
funext i
exact sub_eq_zero.mp (congrFun hv i)
funext j
refine Fin.cases ?_ (fun i => ?_) j
· exact hzero
· exact congrFun hsucc i
VandermondeSynthesis 2 core · 3 supporting This file computes the kernel dimension of a finite moment-synthesis map with distinct complex nodes and one endpoint coordinate. ★ endpointOrderSynthesis_ker_finrank
Vandermonde synthesis maps
This file computes the kernel dimension of a finite moment-synthesis map with distinct complex nodes and one endpoint coordinate.
def endpointOrderSynthesis reviewed
⚑ flagged
Causalean.Mathlib.LinearAlgebra
Given a nonnegative integer , a commutative semiring of coefficients, node values, and a nonnegative integer , the endpoint-order synthesis map sends coefficients to the first moment sums of the node coefficients, with the terminal coefficient added only to the moment of order .
Definition (Lean source)
theorem endpointOrderSynthesis_ker_finrank reviewed
⚑ flagged
Causalean.Mathlib.LinearAlgebra
For natural numbers n, r, a field K, and pairwise distinct nodes s : Fin n → K, the dimension of the kernel of the order-r endpoint synthesis map equals n - r: below the square threshold (r < n) the kernel has dimension n - r, and at or above it (r ≥ n) the kernel is zero, matching n - r = 0 under truncated subtraction.
Formal statement
Proof (Lean source)
theorem endpointOrderSynthesis_ker_finrank {n r : ℕ} {K : Type*} [Field K]
(s : Fin n → K) (hs : Injective s) :
finrank K (ker (endpointOrderSynthesis s r)) = n - r := by
by_cases hr : r < n
· have hsurj := endpointOrderSynthesis_surjective s hs hr
have hrange : range (endpointOrderSynthesis s r) = ⊤ :=
LinearMap.range_eq_top.mpr hsurj
have hnull := LinearMap.finrank_range_add_finrank_ker
(endpointOrderSynthesis s r)
rw [hrange, finrank_top, Module.finrank_pi K, Module.finrank_pi K,
Fintype.card_fin, Fintype.card_fin] at hnull
omega
· have hinj := endpointOrderSynthesis_injective (r := r) s hs (by omega)
rw [LinearMap.ker_eq_bot.mpr hinj, finrank_bot]
omega
3 supporting declarations (lemmas, instances)
-
endpointOrderSynthesis_singlelemma — Applying the moment-synthesis map to the standard basis vector for a node produces the vector of that node's powers across the requested moment orders.hypothesesconclusionendpointOrderSynthesis s r (single j.castSucc 1) = fun a => s j ^ a.valProof (Lean source)
lemma endpointOrderSynthesis_single {n r : ℕ} {K : Type*} [CommSemiring K] (s : Fin n → K) (j : Fin n) : endpointOrderSynthesis s r (single j.castSucc 1) = fun a => s j ^ a.val := by funext a simp only [endpointOrderSynthesis, LinearMap.coe_mk, AddHom.coe_mk] rw [Finset.sum_eq_single j] · simp · intro b _ hb have hcast : b.castSucc ≠ j.castSucc := fun h => hb (Fin.castSucc_injective n h) simp [Pi.single_eq_of_ne hcast] · simp -
endpointOrderSynthesis_surjectivelemma — With distinct node values, the finite moment-synthesis map can reproduce every target vector of moments up through an order smaller than the number of nodes.hypothesesconclusionProof (Lean source)
lemma endpointOrderSynthesis_surjective {n r : ℕ} {K : Type*} [Field K] (s : Fin n → K) (hs : Injective s) (hr : r < n) : Surjective (endpointOrderSynthesis s r) := by let e : Fin (r + 1) → Fin n := fun j => ⟨j, by omega⟩ have he : Injective e := by intro x y h apply Fin.ext simpa [e] using congrArg Fin.val h let A : Matrix (Fin (r + 1)) (Fin (r + 1)) K := (Matrix.vandermonde (s ∘ e)).transpose have hdet : A.det ≠ 0 := by rw [Matrix.det_transpose] exact Matrix.det_vandermonde_ne_zero_iff.mpr (hs.comp he) have hAinj : Injective A.mulVecLin := by intro x y hxy apply sub_eq_zero.mp apply Matrix.eq_zero_of_mulVec_eq_zero hdet change A.mulVec x = A.mulVec y at hxy rw [Matrix.mulVec_sub, hxy, sub_self] let E : (Fin (r + 1) → K) ≃ₗ[K] (Fin (r + 1) → K) := LinearEquiv.ofInjectiveEndo A.mulVecLin hAinj intro y let w : Fin (r + 1) → K := E.symm y let z : Fin (n + 1) → K := ∑ j : Fin (r + 1), w j • (single (e j).castSucc (1 : K) : Fin (n + 1) → K) refine ⟨z, ?_⟩ rw [show z = ∑ j : Fin (r + 1), w j • (single (e j).castSucc (1 : K) : Fin (n + 1) → K) by rfl, map_sum] simp_rw [map_smul, endpointOrderSynthesis_single] have hEy : A.mulVec w = y := E.apply_symm_apply y funext a simp only [Finset.sum_apply, Pi.smul_apply, smul_eq_mul] calc ∑ j : Fin (r + 1), w j * s (e j) ^ a.val = A.mulVec w a := by simp [A, mulVec, dotProduct, Matrix.vandermonde_apply, e, mul_comm] _ = y a := congrFun hEy a -
endpointOrderSynthesis_injectivelemma — With distinct node values, moments through an order at least as large as the number of nodes uniquely determine every coordinate supplied to the moment-synthesis map.hypothesesconclusionProof (Lean source)
lemma endpointOrderSynthesis_injective {n r : ℕ} {K : Type*} [CommRing K] [IsDomain K] (s : Fin n → K) (hs : Injective s) (hr : n ≤ r) : Injective (endpointOrderSynthesis s r) := by intro z z' hzz' apply sub_eq_zero.mp let v := z - z' have hv : endpointOrderSynthesis s r v = 0 := by rw [map_sub, hzz', sub_self] have hfinite : (fun j : Fin n => v j.castSucc) = 0 := by apply Matrix.eq_zero_of_forall_pow_sum_mul_pow_eq_zero hs intro a have ha : a.val < r := lt_of_lt_of_le a.isLt hr have hcoord := congrFun hv ⟨a, by omega⟩ simpa [endpointOrderSynthesis, ha.ne] using hcoord funext j refine Fin.lastCases ?_ (fun i => ?_) j · have hcoord := congrFun hv (last r) have hzero : ∀ i : Fin n, v i.castSucc = 0 := fun i => congrFun hfinite i simpa [v, endpointOrderSynthesis, hzero] using hcoord · exact congrFun hfinite i