Documentation

CompPoly.LinearAlgebra.PolynomialMatrix.MuldersStorjohannCorrectness.Combinations

Mulders-Storjohann Correctness Row Combination Helpers #

Row-linear-combination size, coefficient, and support lemmas.

source
theorem CompPoly.PolynomialMatrix.rowLinearCombination_range_size {F : Type u_1} [Field F] [BEq F] [LawfulBEq F] {M : PolynomialMatrix F} (hM : M.WellFormed) (coeffs : Array (CPolynomial F)) (n : ℕ) :
n ≤ Array.size M → Array.size (List.foldl (fun (acc : PolynomialRow F) (i : ℕ) => rowAdd acc (rowScalePolynomial (coeffs.getD i 0) (Array.getD M i #[]))) (zeroRow M.MatrixWidth) (List.range n)) = M.MatrixWidth
source
theorem CompPoly.PolynomialMatrix.rowLinearCombination_size {F : Type u_1} [Field F] [BEq F] [LawfulBEq F] {M : PolynomialMatrix F} (hM : M.WellFormed) (coeffs : Array (CPolynomial F)) :
Array.size (rowLinearCombination coeffs M) = M.MatrixWidth
source
def CompPoly.PolynomialMatrix.rowCombinationTermSupport {F : Type u_1} [Field F] [BEq F] [DecidableEq F] (coeffs : Array (CPolynomial F)) (M : PolynomialMatrix F) (shift : Array ℕ) :
Finset ℕ
Instances For
    source
    def CompPoly.PolynomialMatrix.rowCombinationTermDegree {F : Type u_1} [Field F] [BEq F] (coeffs : Array (CPolynomial F)) (M : PolynomialMatrix F) (shift : Array ℕ) (i : ℕ) :
    ℕ
    Instances For
      source
      def CompPoly.PolynomialMatrix.rowCombinationTermPosition {F : Type u_1} [Field F] [BEq F] (M : PolynomialMatrix F) (shift : Array ℕ) (i : ℕ) :
      ℕ
      Instances For
        source
        theorem CompPoly.PolynomialMatrix.rowGet_rowLinearCombination_range_coeff {F : Type u_1} [Field F] [BEq F] [LawfulBEq F] {M : PolynomialMatrix F} (coeffs : Array (CPolynomial F)) (j k n : ℕ) :
        (rowGet (List.foldl (fun (acc : PolynomialRow F) (i : ℕ) => rowAdd acc (rowScalePolynomial (coeffs.getD i 0) (Array.getD M i #[]))) (zeroRow M.MatrixWidth) (List.range n)) j).coeff k = ∑ i ∈ Finset.range n, (coeffs.getD i 0 * rowGet (Array.getD M i #[]) j).coeff k
        source
        theorem CompPoly.PolynomialMatrix.rowGet_rowLinearCombination_coeff {F : Type u_1} [Field F] [BEq F] [LawfulBEq F] {M : PolynomialMatrix F} (coeffs : Array (CPolynomial F)) (j k : ℕ) :
        (rowGet (rowLinearCombination coeffs M) j).coeff k = ∑ i ∈ Finset.range (Array.size M), (coeffs.getD i 0 * rowGet (Array.getD M i #[]) j).coeff k
        source
        theorem CompPoly.PolynomialMatrix.rowLinearCombination_range_eq_zeroRow_of_forall_zero_or_row_zero {F : Type u_1} [Field F] [BEq F] [LawfulBEq F] {M : PolynomialMatrix F} (hM : M.WellFormed) (coeffs : Array (CPolynomial F)) (hzero : ∀ i < Array.size M, coeffs.getD i 0 = 0 ∨ RowIsZero (Array.getD M i #[])) (n : ℕ) :
        n ≤ Array.size M → List.foldl (fun (acc : PolynomialRow F) (i : ℕ) => rowAdd acc (rowScalePolynomial (coeffs.getD i 0) (Array.getD M i #[]))) (zeroRow M.MatrixWidth) (List.range n) = zeroRow M.MatrixWidth
        source
        theorem CompPoly.PolynomialMatrix.rowLinearCombination_eq_zeroRow_of_forall_zero_or_row_zero {F : Type u_1} [Field F] [BEq F] [LawfulBEq F] {M : PolynomialMatrix F} (hM : M.WellFormed) (coeffs : Array (CPolynomial F)) (hzero : ∀ i < Array.size M, coeffs.getD i 0 = 0 ∨ RowIsZero (Array.getD M i #[])) :
        rowLinearCombination coeffs M = zeroRow M.MatrixWidth
        source
        theorem CompPoly.PolynomialMatrix.rowCombinationTermSupport_nonempty_of_combination_degree_some {F : Type u_1} [Field F] [BEq F] [LawfulBEq F] [DecidableEq F] {M : PolynomialMatrix F} {shift : Array ℕ} (hM : M.WellFormed) {coeffs : Array (CPolynomial F)} {rowDeg : ℕ} (hdeg : rowShiftedDegree? (rowLinearCombination coeffs M) shift = some rowDeg) :
        (rowCombinationTermSupport coeffs M shift).Nonempty