Mathlib.LinearAlgebra
Linear-algebra helpers staged for Mathlib: monomial-matrix and generalized-permutation lemmas used by causal-discovery identification proofs.
PerronFrobenius 15 core · 26 supporting · 1 submodule Perron–Frobenius results for finite positive linear systems. Tensor 40 core · 27 supporting · 1 submodule Tensor methods for finite symmetric rank-one decompositions, centered on contraction pencils, their simultaneous diagonalization and conditioning, and quantitative factor recovery from tensors of order d + d + q.
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 of a positive-definite matrix has unit diagonal, including at the selected diagonal position.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 — Every LDL diagonal entry of a real positive-definite matrix is strictly positive, including at the selected position.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 — The Gram-Schmidt lower-inverse of a positive-definite matrix is lower-triangular.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 — The inverse lower factor of a positive-definite matrix 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 — The inverse lower factor of a positive-definite matrix has unit diagonal, including at the selected diagonal position.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 — If a matrix is orthogonal, upper-triangular, and has strictly positive diagonal, it 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 nodes over a field, 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 nodes over a field, 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 index in either block receives a doubled exponent 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 its coefficient for the supplied coefficient vector and index.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 for the supplied vector.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 whenever the number of positions 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 doubled coefficient polynomial gives the coefficient-weighted sum of powers for the supplied coefficients and 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 doubled coefficient polynomial gives the sum weighted by derivative monomial values for the supplied coefficients and evaluation point.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 two-block coefficient vector is zero when its polynomial vanishes together with its derivative on a nonempty finite node family whose nodes are pairwise distinct.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) : (X - 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 => (X - 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, (X - 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, (X - C (s i)) ^ 2).natDegree = 2 * n := by calc _ = ∑ i : Fin n, ((X - 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 — Every positive-node index embeds away from the distinguished zero node when the node family is nonempty.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 index in either pinned block receives an exponent 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 its coefficient for the supplied coefficient vector and index.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 for the supplied vector.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 whenever the number of nodes is positive.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 gives the coefficient-weighted sum of pinned powers for the supplied coefficients and evaluation point.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 gives the sum weighted by derivative monomial values for the supplied coefficients and evaluation 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 pinned coefficient vector is zero when its polynomial vanishes at every node and its derivative vanishes at every nondistinguished node in a nonempty finite node family whose nodes are pairwise distinct.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 := X - C (s ⟨0, hn⟩) let rest : Fin (n - 1) → Polynomial K := fun i => (X - 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)
ContinuousSolution 2 core · 5 supporting This file gives an anchored local solver for a continuous family of finite real linear systems. ★ exists_local_anchoredSolution_of_surjective
Local continuous solutions of full-row-rank linear systems
This file gives an anchored local solver for a continuous family of finite real linear systems. A right inverse chosen at the base parameter keeps the square correction matrix nonsingular nearby, so the solver remains continuous while preserving the prescribed base solution.
def anchoredSolution reviewed
⚑ flagged
Causalean.Mathlib.LinearAlgebra
Given a coefficient family, right-hand-side family, fixed correction matrix, prescribed base vector, and parameter, the anchored solution is the base vector plus the inverse-based correction at that parameter.
theorem exists_local_anchoredSolution_of_surjective reviewed
⚑ flagged
Causalean.Mathlib.LinearAlgebra
A coefficient family, right-hand-side family, base parameter, and prescribed base solution, with continuous coefficients, a continuous right-hand side, full row rank at the base, and a solved base system, have an open neighborhood with a continuous solution through the prescribed base solution.
Formal statement
hypotheses
X :
Type u_1
k :
ℕ
n :
ℕ
b :
X → Fin k → ℝ
x₀ :
X
y₀ :
Fin n → ℝ
hA :
hb :
hfull :
Surjective (A x₀).mulVec
hy :
A x₀ *ᵥ y₀ = b x₀
conclusion
conclusion 1
x ∈ s :
A x *ᵥ y x = b x
Proof (Lean source)
theorem exists_local_anchoredSolution_of_surjective
(A : X → Matrix (Fin k) (Fin n) ℝ) (b : X → Fin k → ℝ)
(x₀ : X) (y₀ : Fin n → ℝ)
(hA : Continuous A) (hb : Continuous b)
(hfull : Surjective (A x₀).mulVec)
(hy : A x₀ *ᵥ y₀ = b x₀) :
∃ (s : Set X) (y : X → Fin n → ℝ),
IsOpen s ∧ x₀ ∈ s ∧ ContinuousOn y s ∧
y x₀ = y₀ ∧ ∀ x ∈ s, A x *ᵥ y x = b x := by
obtain ⟨R₀, hR⟩ := Matrix.mulVec_surjective_iff_exists_right_inverse.mp hfull
obtain ⟨s, hsOpen, hx₀, hContinuous, hy₀, hSolution⟩ :=
exists_local_anchoredSolution_of_rightInverse A b R₀ x₀ y₀ hA hb hR hy
exact ⟨s, anchoredSolution A b R₀ y₀, hsOpen, hx₀, hContinuous, hy₀, hSolution⟩
5 supporting declarations (lemmas, instances)
-
anchoredSolution_eq_of_det_ne_zerotheorem — A coefficient family, right-hand-side family, fixed correction matrix, base vector, and parameter, under a nonzero determinant of the correction matrix, have an anchored solution that solves the linear system at that parameter.hypothesesX :sharedType u_1k :sharedℕn :sharedℕb :X → Fin k → ℝy₀ :Fin n → ℝx :Xhx :(A x * R₀).det ≠ 0conclusionA x *ᵥ anchoredSolution A b R₀ y₀ x = b xProof (Lean source)
theorem anchoredSolution_eq_of_det_ne_zero (A : X → Matrix (Fin k) (Fin n) ℝ) (b : X → Fin k → ℝ) (R₀ : Matrix (Fin n) (Fin k) ℝ) (y₀ : Fin n → ℝ) (x : X) (hx : (A x * R₀).det ≠ 0) : A x *ᵥ anchoredSolution A b R₀ y₀ x = b x := by unfold anchoredSolution rw [Matrix.mulVec_add, Matrix.mulVec_mulVec, Matrix.mulVec_mulVec, Matrix.mul_nonsing_inv _ (isUnit_iff_ne_zero.mpr hx), Matrix.one_mulVec] abel -
anchoredSolution_at_basetheorem — A coefficient family, right-hand-side family, fixed correction matrix, prescribed base solution, and base parameter, with a right-inverse identity at the base and a solved base system, have an anchored solution equal to the prescribed base solution at the base parameter.hypothesesX :sharedType u_1k :sharedℕn :sharedℕb :X → Fin k → ℝy₀ :Fin n → ℝx₀ :XhR :A x₀ * R₀ = 1hy :A x₀ *ᵥ y₀ = b x₀conclusionanchoredSolution A b R₀ y₀ x₀ = y₀Proof (Lean source)
theorem anchoredSolution_at_base (A : X → Matrix (Fin k) (Fin n) ℝ) (b : X → Fin k → ℝ) (R₀ : Matrix (Fin n) (Fin k) ℝ) (y₀ : Fin n → ℝ) (x₀ : X) (hR : A x₀ * R₀ = 1) (hy : A x₀ *ᵥ y₀ = b x₀) : anchoredSolution A b R₀ y₀ x₀ = y₀ := by simp [anchoredSolution, hy, hR] -
continuousAt_anchoredSolutiontheorem — A coefficient family, right-hand-side family, fixed correction matrix, base vector, and parameter, with continuous coefficients, a continuous right-hand side, and a nonsingular correction matrix at that parameter, have an anchored solution continuous at that parameter.hypothesesX :sharedType u_1k :sharedℕn :sharedℕb :X → Fin k → ℝy₀ :Fin n → ℝx :XhA :hb :hx :(A x * R₀).det ≠ 0conclusionContinuousAt (anchoredSolution A b R₀ y₀) xProof (Lean source)
theorem continuousAt_anchoredSolution [TopologicalSpace X] (A : X → Matrix (Fin k) (Fin n) ℝ) (b : X → Fin k → ℝ) (R₀ : Matrix (Fin n) (Fin k) ℝ) (y₀ : Fin n → ℝ) (x : X) (hA : Continuous A) (hb : Continuous b) (hx : (A x * R₀).det ≠ 0) : ContinuousAt (anchoredSolution A b R₀ y₀) x := by have hM : Continuous (fun z => A z * R₀) := hA.matrix_mul continuous_const have hInv : ContinuousAt (fun z => (A z * R₀)⁻¹) x := by have hringInv : ContinuousAt Ring.inverse (A x * R₀).det := by rw [show (Ring.inverse : ℝ → ℝ) = inv from funext Ring.inverse_eq_inv] exact continuousAt_inv₀ hx exact ContinuousAt.comp' (f := fun z => A z * R₀) (continuousAt_matrix_inv (A x * R₀) hringInv) hM.continuousAt have hResidual : Continuous (fun z => b z - A z *ᵥ y₀) := hb.sub (hA.matrix_mulVec continuous_const) have hInner : ContinuousAt (fun z => (A z * R₀)⁻¹ *ᵥ (b z - A z *ᵥ y₀)) x := (continuous_fst.matrix_mulVec continuous_snd).continuousAt.comp (hInv.prodMk hResidual.continuousAt) have hCorrection : ContinuousAt (fun z => R₀ *ᵥ ((A z * R₀)⁻¹ *ᵥ (b z - A z *ᵥ y₀))) x := (continuous_const.matrix_mulVec continuous_id).continuousAt.comp hInner change ContinuousAt (fun z => y₀ + R₀ *ᵥ ((A z * R₀)⁻¹ *ᵥ (b z - A z *ᵥ y₀))) x exact continuousAt_const.add hCorrection -
isOpen_nonSingular_settheorem — A coefficient family and fixed correction matrix, with continuous coefficients, have an open set of parameters where the correction matrix is nonsingular.hypothesesX :sharedType u_1k :sharedℕn :sharedℕhA :conclusionIsOpen {x : X | (A x * R₀).det ≠ 0}Proof (Lean source)
theorem isOpen_nonSingular_set [TopologicalSpace X] (A : X → Matrix (Fin k) (Fin n) ℝ) (R₀ : Matrix (Fin n) (Fin k) ℝ) (hA : Continuous A) : IsOpen {x : X | (A x * R₀).det ≠ 0} := by have hdet : Continuous (fun x => (A x * R₀).det) := (hA.matrix_mul continuous_const).matrix_det simpa only [Set.preimage_ofPred_eq] using (isOpen_ne (x := (0 : ℝ))).preimage hdet -
exists_local_anchoredSolution_of_rightInversetheorem — A coefficient family, right-hand-side family, fixed correction matrix, base parameter, and prescribed base solution, with continuous coefficients, a continuous right-hand side, a right inverse at the base, and a solved base system, have an open neighborhood carrying a continuous anchored solution that agrees at the base and solves every system in the neighborhood.hypothesesX :sharedType u_1k :sharedℕn :sharedℕb :X → Fin k → ℝx₀ :Xy₀ :Fin n → ℝhA :hb :hR :A x₀ * R₀ = 1hy :A x₀ *ᵥ y₀ = b x₀conclusion∃ s : Set X,Proof (Lean source)
theorem exists_local_anchoredSolution_of_rightInverse (A : X → Matrix (Fin k) (Fin n) ℝ) (b : X → Fin k → ℝ) (R₀ : Matrix (Fin n) (Fin k) ℝ) (x₀ : X) (y₀ : Fin n → ℝ) (hA : Continuous A) (hb : Continuous b) (hR : A x₀ * R₀ = 1) (hy : A x₀ *ᵥ y₀ = b x₀) : ∃ s : Set X, IsOpen s ∧ x₀ ∈ s ∧ ContinuousOn (anchoredSolution A b R₀ y₀) s ∧ anchoredSolution A b R₀ y₀ x₀ = y₀ ∧ ∀ x ∈ s, A x *ᵥ anchoredSolution A b R₀ y₀ x = b x := by refine ⟨{x | (A x * R₀).det ≠ 0}, isOpen_nonSingular_set A R₀ hA, ?_, ?_, anchoredSolution_at_base A b R₀ y₀ x₀ hR hy, ?_⟩ · change (A x₀ * R₀).det ≠ 0 rw [hR] simp · exact continuousOn_of_forall_continuousAt fun x hx => continuousAt_anchoredSolution A b R₀ y₀ x hA hb hx · intro x hx exact anchoredSolution_eq_of_det_ne_zero A b R₀ y₀ x hx
MonomialMatrix 3 core · 0 supporting A generalized-permutation (monomial) matrix has exactly one non-zero entry in each row and column — equivalently, it is a permutation matrix composed with an invertible diagonal rescaling. ★ genPerm_of_det_ne_zero_of_colSupport★ perm_uniqueness★ eq_of_genPerm_triangular_unitDiag
Generalized-permutation (monomial) matrices
A generalized-permutation (monomial) matrix has exactly one non-zero entry in each row and column — equivalently, it is a permutation matrix composed with an invertible diagonal rescaling. These matrices form a group, and this file collects three facts about it.
1. An invertible matrix with at most one non-zero entry per column is automatically of 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. 3. Two unit-diagonal matrices related by a generalized permutation, one of them lower-triangular with respect to some ordering of the indices, are equal — triangularity plus a unit diagonal forces the permutation to be the identity and every scaling to be one.
The third fact is a rigidity statement: within the generalized-permutation orbit of a matrix, triangularity with respect to an ordering pins down a unique representative.
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
Triangular representative of a generalized-permutation orbit. 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 for some ordering σ of the indices (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.
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]
NormalEquations 3 core · 2 supporting Normal equations and projection-optimality identities for weighted linear least-squares fits with nonnegative weights. ★ lstsq_normal_equations
Normal equations for weighted linear least squares
Normal equations and projection-optimality identities for weighted linear least-squares fits with nonnegative weights.
Given a real matrix Φ, a vector Y, and nonnegative weights w, a weighted linear
least-squares fit is a coefficient vector c minimizing ∑ᵢ wᵢ (Yᵢ − ∑ⱼ cⱼ Φᵢⱼ)². This file
proves the first-order optimality conditions — the normal equations
∑ᵢ wᵢ (Yᵢ − ∑ⱼ cⱼ Φᵢⱼ) Φᵢₖ = 0 for every column index k,
directly from global minimality, with no differentiability API: the objective is quadratic along each coordinate direction, so a one-variable perturbation forces the linear coefficient to vanish. The file also proves the Pythagorean identity and the comparison consequence that an orthogonal residual is optimal.
Everything here is stated for an arbitrary Φ; no design family is privileged.
def lstsqResidual reviewed
⚑ flagged
Causalean.Mathlib.LinearAlgebra.NormalEquations
Given a sample indexed by a nonnegative number of observations, a finite collection of basis indices, a real-valued design array, real-valued outcomes, real-valued coefficients indexed by the basis, and an observation in the sample, the least-squares residual for that observation is its outcome minus the fitted value .
def lstsqObjective reviewed
⚑ flagged
Causalean.Mathlib.LinearAlgebra.NormalEquations
Given a sample indexed by a nonnegative number of observations, a finite collection of basis indices, a real-valued design array, real-valued observation weights, real-valued outcomes, and real-valued coefficients indexed by the basis, the weighted least-squares objective is , where is the residual of observation under those coefficients.
Definition (Lean source)
theorem lstsq_normal_equations reviewed
⚑ flagged
Causalean.Mathlib.LinearAlgebra.NormalEquations
Normal equations for weighted linear least squares. If the weights w are nonnegative and the coefficient vector c globally minimizes the weighted sum of squares ∑ᵢ wᵢ (Yᵢ − ∑ⱼ cⱼ Φᵢⱼ)² over all coefficient vectors, then the weighted residual is orthogonal to every design column: ∑ᵢ wᵢ (Yᵢ − ∑ⱼ cⱼ Φᵢⱼ) Φᵢₖ = 0 for each basis index k.
Formal statement
hypotheses
N :
ℕ
w Y :
Fin N → ℝ
c :
ι → ℝ
hw :
∀ i, 0 ≤ w i
hmin :
∀ c' : ι → ℝ, lstsqObjective Φ w Y c ≤ lstsqObjective Φ w Y c'
k :
ι
conclusion
∑ i, w i * lstsqResidual Φ Y c i * Φ i k = 0
Proof (Lean source)
theorem lstsq_normal_equations {N : ℕ} {ι : Type*} [Fintype ι]
{Φ : Fin N → ι → ℝ} {w Y : Fin N → ℝ} {c : ι → ℝ}
(hw : ∀ i, 0 ≤ w i)
(hmin : ∀ c' : ι → ℝ, lstsqObjective Φ w Y c ≤ lstsqObjective Φ w Y c') :
∀ k : ι, ∑ i, w i * lstsqResidual Φ Y c i * Φ i k = 0 := by
intro k
classical
let r : Fin N → ℝ := fun i => lstsqResidual Φ Y c i
let A : ℝ := ∑ i, w i * r i * Φ i k
let B : ℝ := ∑ i, w i * (Φ i k) ^ 2
have hres_update (s : ℝ) (i : Fin N) :
lstsqResidual Φ Y (update c k (c k + s)) i =
r i - s * Φ i k := by
unfold lstsqResidual
dsimp [r]
have hfun :
(fun j : ι => update c k (c k + s) j * Φ i j) =
update (fun j : ι => c j * Φ i j) k ((c k + s) * Φ i k) := by
funext j
by_cases hj : j = k
· subst hj
simp
· simp [update, hj]
have hsum :
(∑ j : ι, update c k (c k + s) j * Φ i j) =
(∑ j : ι, c j * Φ i j) + s * Φ i k := by
rw [hfun, sum_update_univ_eq_sub_add]
ring
rw [hsum]
change Y i - ((∑ j : ι, c j * Φ i j) + s * Φ i k) =
(Y i - ∑ j : ι, c j * Φ i j) - s * Φ i k
ring
have hobj (s : ℝ) :
lstsqObjective Φ w Y (update c k (c k + s)) =
lstsqObjective Φ w Y c - 2 * s * A + s ^ 2 * B := by
unfold lstsqObjective
calc
(∑ i, w i * lstsqResidual Φ Y (update c k (c k + s)) i ^ 2) =
∑ i, (w i * r i ^ 2 - 2 * s * (w i * r i * Φ i k) +
s ^ 2 * (w i * (Φ i k) ^ 2)) := by
apply Finset.sum_congr rfl
intro i hi
rw [hres_update s i]
ring
_ = (∑ i, w i * lstsqResidual Φ Y c i ^ 2) - 2 * s * A + s ^ 2 * B := by
simp [Finset.sum_sub_distrib, Finset.sum_add_distrib, Finset.mul_sum, A, B, r]
have hquad : ∀ s : ℝ, 0 ≤ -2 * s * A + s ^ 2 * B := by
intro s
have h := hmin (update c k (c k + s))
rw [hobj s] at h
linarith
have hB : 0 ≤ B := by
dsimp [B]
apply Finset.sum_nonneg
intro i hi
exact mul_nonneg (hw i) (sq_nonneg _)
exact linear_coeff_eq_zero_of_quadratic_nonneg hB hquad
2 supporting declarations (lemmas, instances)
-
lstsq_pythagorastheorem — Pythagorean decomposition for weighted least squares. If the residual at c is orthogonal to every design column, then for any coefficient vector c' the weighted sum of squares splits as its value at c plus the weighted squared fitted-value difference. The orthogonality condition holds, for example, when c is a least-squares minimizer by lstsq_normal_equations.hypothesesN :ℕw Y :Fin N → ℝc :ι → ℝhortho :∀ k : ι, ∑ i, w i * lstsqResidual Φ Y c i * Φ i k = 0c' :ι → ℝconclusionlstsqObjective Φ w Y c'= lstsqObjective Φ w Y c + ∑ i, w i * (∑ j, (c j - c' j) * Φ i j) ^ 2Proof (Lean source)
theorem lstsq_pythagoras {N : ℕ} {ι : Type*} [Fintype ι] {Φ : Fin N → ι → ℝ} {w Y : Fin N → ℝ} {c : ι → ℝ} (hortho : ∀ k : ι, ∑ i, w i * lstsqResidual Φ Y c i * Φ i k = 0) (c' : ι → ℝ) : lstsqObjective Φ w Y c' = lstsqObjective Φ w Y c + ∑ i, w i * (∑ j, (c j - c' j) * Φ i j) ^ 2 := by classical let d : Fin N → ℝ := fun i => ∑ j, (c j - c' j) * Φ i j have hkey : ∀ i, lstsqResidual Φ Y c' i = lstsqResidual Φ Y c i + d i := by intro i unfold lstsqResidual dsimp [d] calc Y i - ∑ j, c' j * Φ i j = (Y i - ∑ j, c j * Φ i j) + ((∑ j, c j * Φ i j) - ∑ j, c' j * Φ i j) := by ring _ = (Y i - ∑ j, c j * Φ i j) + ∑ j, (c j - c' j) * Φ i j := by congr 1 rw [← Finset.sum_sub_distrib] apply Finset.sum_congr rfl intro j hj ring have hcross : (∑ i, w i * lstsqResidual Φ Y c i * d i) = 0 := by dsimp [d] calc (∑ i, w i * lstsqResidual Φ Y c i * (∑ j, (c j - c' j) * Φ i j)) = ∑ i, ∑ j, (c j - c' j) * (w i * lstsqResidual Φ Y c i * Φ i j) := by apply Finset.sum_congr rfl intro i hi rw [Finset.mul_sum] apply Finset.sum_congr rfl intro j hj ring _ = ∑ j, ∑ i, (c j - c' j) * (w i * lstsqResidual Φ Y c i * Φ i j) := by rw [Finset.sum_comm] _ = ∑ j, (c j - c' j) * (∑ i, w i * lstsqResidual Φ Y c i * Φ i j) := by apply Finset.sum_congr rfl intro j hj rw [Finset.mul_sum] _ = 0 := by simp [hortho] unfold lstsqObjective have hsum : (∑ i, w i * lstsqResidual Φ Y c' i ^ 2) = (∑ i, w i * lstsqResidual Φ Y c i ^ 2) + 2 * (∑ i, w i * lstsqResidual Φ Y c i * d i) + ∑ i, w i * d i ^ 2 := by calc (∑ i, w i * lstsqResidual Φ Y c' i ^ 2) = ∑ i, (w i * lstsqResidual Φ Y c i ^ 2 + 2 * (w i * lstsqResidual Φ Y c i * d i) + w i * d i ^ 2) := by apply Finset.sum_congr rfl intro i hi rw [hkey i] ring _ = (∑ i, w i * lstsqResidual Φ Y c i ^ 2) + 2 * (∑ i, w i * lstsqResidual Φ Y c i * d i) + ∑ i, w i * d i ^ 2 := by rw [Finset.sum_add_distrib, Finset.sum_add_distrib, Finset.mul_sum] rw [hsum, hcross] dsimp [d] ring -
lstsq_objective_le_of_orthogonaltheorem — Optimality of the orthogonal least-squares fit. If the weights are nonnegative and the residual at c is orthogonal to every design column, then for any coefficient vector c', c has no larger weighted sum of squares. This follows from lstsq_pythagoras because its excess term is nonnegative.hypothesesN :ℕw Y :Fin N → ℝc :ι → ℝhw :∀ i, 0 ≤ w ihortho :∀ k : ι, ∑ i, w i * lstsqResidual Φ Y c i * Φ i k = 0c' :ι → ℝconclusionlstsqObjective Φ w Y c ≤ lstsqObjective Φ w Y c'Proof (Lean source)
theorem lstsq_objective_le_of_orthogonal {N : ℕ} {ι : Type*} [Fintype ι] {Φ : Fin N → ι → ℝ} {w Y : Fin N → ℝ} {c : ι → ℝ} (hw : ∀ i, 0 ≤ w i) (hortho : ∀ k : ι, ∑ i, w i * lstsqResidual Φ Y c i * Φ i k = 0) (c' : ι → ℝ) : lstsqObjective Φ w Y c ≤ lstsqObjective Φ w Y c' := by rw [lstsq_pythagoras hortho c'] have hnn : 0 ≤ ∑ i, w i * (∑ j, (c j - c' j) * Φ i j) ^ 2 := Finset.sum_nonneg (fun i _ => mul_nonneg (hw i) (sq_nonneg _)) linarith
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. ★ exists_weights_stackedContraction_injective
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 exists_weights_stackedContraction_injective reviewed
⚑ flagged
Causalean.Mathlib.LinearAlgebra
For a commutative integral domain K, at least three indices N + 1 (2 ≤ N), and slope values slopes : Fin (N + 1) → K that are pairwise distinct, 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 exists_weights_stackedContraction_injective {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 nodes over a field and one endpoint coordinate. ★ endpointOrderSynthesis_ker_finrank
Vandermonde synthesis maps
This file computes the kernel dimension of a finite moment-synthesis map with distinct nodes over a field 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)
parameters
given by
clause 2
map_add' x y := by funext a simp only [Pi.add_apply, add_mul, Finset.sum_add_distrib] split <;> ring
clause 3
map_smul' c x := by funext a simp only [Pi.smul_apply, smul_eq_mul, RingHom.id_apply] split <;> (simp [← Finset.mul_sum, mul_assoc] <;> ring)
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 — The standard-basis vector for a selected node is sent by the moment-synthesis map determined by the nodes to the vector of that node's powers.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 — The moment-synthesis map for the supplied nodes covers every target vector when the nodes are pairwise distinct and the requested order is below their number.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 — The moment-synthesis map for the supplied nodes uniquely determines its input when the nodes are pairwise distinct and the requested order is at least their number.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