Mulders-Storjohann Correctness Shifted Leading Term Helpers #
Shifted leading-position data and cancellation degree bounds.
theorem
CompPoly.PolynomialMatrix.rowShiftedLeadingPosition?_lt
{F : Type u_1}
[Field F]
[BEq F]
{row : PolynomialRow F}
{shift : Array ℕ}
{pos : ℕ}
(hpos : rowShiftedLeadingPosition? row shift = some pos)
:
theorem
CompPoly.PolynomialMatrix.rowShiftedLeadingPosition?_no_larger_tie
{F : Type u_1}
[Field F]
[BEq F]
{row : PolynomialRow F}
{shift : Array ℕ}
{degree pos k : ℕ}
(hdeg : rowShiftedDegree? row shift = some degree)
(hpos : rowShiftedLeadingPosition? row shift = some pos)
(hk : k < Array.size row)
(hposk : pos < k)
:
theorem
CompPoly.PolynomialMatrix.list_find?_some_of_exists
{α : Type u_2}
(xs : List α)
(pred : α → Bool)
(hexists : ∃ x ∈ xs, pred x = true)
:
∃ (x : α), List.find? pred xs = some x
theorem
CompPoly.PolynomialMatrix.rowShiftedLeadingPosition?_some_of_degree
{F : Type u_1}
[Field F]
[BEq F]
{row : PolynomialRow F}
{shift : Array ℕ}
{degree : ℕ}
(hdeg : rowShiftedDegree? row shift = some degree)
:
∃ (pos : ℕ), rowShiftedLeadingPosition? row shift = some pos
theorem
CompPoly.PolynomialMatrix.rowShiftedLeadingPosition?_le_of_entry_eq_degree
{F : Type u_1}
[Field F]
[BEq F]
{row : PolynomialRow F}
{shift : Array ℕ}
{degree pos k : ℕ}
(hdeg : rowShiftedDegree? row shift = some degree)
(hpos : rowShiftedLeadingPosition? row shift = some pos)
(hk : k < Array.size row)
(hentry : shiftedEntryDegree? row shift k = some degree)
:
theorem
CompPoly.PolynomialMatrix.rowShiftedDegree?_entry_bound
{F : Type u_1}
[Field F]
[BEq F]
[LawfulBEq F]
{row : PolynomialRow F}
{shift : Array ℕ}
{degree j : ℕ}
(hdeg : rowShiftedDegree? row shift = some degree)
(hj : j < Array.size row)
(hne : rowGet row j ≠ 0)
:
theorem
CompPoly.PolynomialMatrix.rowShiftedLeadingPosition?_entry_eq
{F : Type u_1}
[Field F]
[BEq F]
{row : PolynomialRow F}
{shift : Array ℕ}
{degree pos : ℕ}
(hdeg : rowShiftedDegree? row shift = some degree)
(hpos : rowShiftedLeadingPosition? row shift = some pos)
:
theorem
CompPoly.PolynomialMatrix.rowShiftedLeadingTerm?_some_of_position
{F : Type u_1}
[Field F]
[BEq F]
[LawfulBEq F]
{row : PolynomialRow F}
{shift : Array ℕ}
{pos : ℕ}
(hpos : rowShiftedLeadingPosition? row shift = some pos)
:
∃ (term : ShiftedLeadingTerm F), rowShiftedLeadingTerm? row shift = some term ∧ term.position = pos
theorem
CompPoly.PolynomialMatrix.rowShiftedLeadingTerm?_some_data
{F : Type u_1}
[Field F]
[BEq F]
[LawfulBEq F]
{row : PolynomialRow F}
{shift : Array ℕ}
{term : ShiftedLeadingTerm F}
(hterm : rowShiftedLeadingTerm? row shift = some term)
:
rowShiftedDegree? row shift = some term.shiftedDegree ∧ rowShiftedLeadingPosition? row shift = some term.position ∧ rowGet row term.position ≠ 0 ∧ term.degree = (rowGet row term.position).natDegree ∧ term.shiftedDegree = term.degree + shift.getD term.position 0 ∧ term.coeff = (rowGet row term.position).coeff term.degree
theorem
CompPoly.PolynomialMatrix.rowShiftedLeadingTerm?_coeff_ne_zero
{F : Type u_1}
[Field F]
[BEq F]
[LawfulBEq F]
{row : PolynomialRow F}
{shift : Array ℕ}
{term : ShiftedLeadingTerm F}
(hterm : rowShiftedLeadingTerm? row shift = some term)
:
theorem
CompPoly.PolynomialMatrix.cpoly_natDegree_monomial_le
{F : Type u_1}
[Field F]
[BEq F]
[LawfulBEq F]
[DecidableEq F]
(d : ℕ)
(c : F)
:
theorem
CompPoly.PolynomialMatrix.cpoly_natDegree_monomial_mul_le
{F : Type u_1}
[Field F]
[BEq F]
[LawfulBEq F]
[DecidableEq F]
(d : ℕ)
(c : F)
(P : CPolynomial F)
:
theorem
CompPoly.PolynomialMatrix.cpoly_coeff_monomial_mul
{F : Type u_1}
[Field F]
[BEq F]
[LawfulBEq F]
[DecidableEq F]
(n d : ℕ)
(c : F)
(P : CPolynomial F)
:
theorem
CompPoly.PolynomialMatrix.rowShiftedDegree?_le_of_entry_bound
{F : Type u_1}
[Field F]
[BEq F]
[LawfulBEq F]
{row : PolynomialRow F}
{shift : Array ℕ}
{degree bound : ℕ}
(hbound : ∀ k < Array.size row, rowGet row k ≠ 0 → (rowGet row k).natDegree + shift.getD k 0 ≤ bound)
(hdeg : rowShiftedDegree? row shift = some degree)
:
theorem
CompPoly.PolynomialMatrix.rowShiftedLeadingTerm?_entry_bound
{F : Type u_1}
[Field F]
[BEq F]
[LawfulBEq F]
{row : PolynomialRow F}
{shift : Array ℕ}
{term : ShiftedLeadingTerm F}
(hterm : rowShiftedLeadingTerm? row shift = some term)
{k : ℕ}
(hk : k < Array.size row)
(hne : rowGet row k ≠ 0)
:
theorem
CompPoly.PolynomialMatrix.rowShiftedLeadingTerm?_entry_strict_of_pos_lt
{F : Type u_1}
[Field F]
[BEq F]
[LawfulBEq F]
{row : PolynomialRow F}
{shift : Array ℕ}
{term : ShiftedLeadingTerm F}
(hterm : rowShiftedLeadingTerm? row shift = some term)
{k : ℕ}
(hk : k < Array.size row)
(hposlt : term.position < k)
(hne : rowGet row k ≠ 0)
:
theorem
CompPoly.PolynomialMatrix.rowScaleMonomial_entry_bound_of_leading_terms
{F : Type u_1}
[Field F]
[BEq F]
[LawfulBEq F]
[DecidableEq F]
{target reducer : PolynomialRow F}
{shift : Array ℕ}
{t r : ShiftedLeadingTerm F}
(ht : rowShiftedLeadingTerm? target shift = some t)
(hr : rowShiftedLeadingTerm? reducer shift = some r)
(hpos : t.position = r.position)
(hle : r.shiftedDegree ≤ t.shiftedDegree)
{k : ℕ}
(hk : k < Array.size reducer)
(hne : rowGet (rowScaleMonomial (t.coeff / r.coeff) (t.degree - r.degree) reducer) k ≠ 0)
:
theorem
CompPoly.PolynomialMatrix.rowScaleMonomial_entry_strict_of_pos_lt
{F : Type u_1}
[Field F]
[BEq F]
[LawfulBEq F]
[DecidableEq F]
{target reducer : PolynomialRow F}
{shift : Array ℕ}
{t r : ShiftedLeadingTerm F}
(ht : rowShiftedLeadingTerm? target shift = some t)
(hr : rowShiftedLeadingTerm? reducer shift = some r)
(hpos : t.position = r.position)
(hle : r.shiftedDegree ≤ t.shiftedDegree)
{k : ℕ}
(hk : k < Array.size reducer)
(hposlt : t.position < k)
(hne : rowGet (rowScaleMonomial (t.coeff / r.coeff) (t.degree - r.degree) reducer) k ≠ 0)
:
theorem
CompPoly.PolynomialMatrix.cancelShiftedLeadingTerm_coeff_cancel
{F : Type u_1}
[Field F]
[BEq F]
[LawfulBEq F]
[DecidableEq F]
{target reducer : PolynomialRow F}
{shift : Array ℕ}
{t r : ShiftedLeadingTerm F}
(ht : rowShiftedLeadingTerm? target shift = some t)
(hr : rowShiftedLeadingTerm? reducer shift = some r)
(hpos : t.position = r.position)
(hle : r.shiftedDegree ≤ t.shiftedDegree)
(hrcoeff : r.coeff ≠ 0)
:
theorem
CompPoly.PolynomialMatrix.cancelShiftedLeadingTerm_no_target_shifted_entry
{F : Type u_1}
[Field F]
[BEq F]
[LawfulBEq F]
[DecidableEq F]
{target reducer : PolynomialRow F}
{shift : Array ℕ}
{t r : ShiftedLeadingTerm F}
(ht : rowShiftedLeadingTerm? target shift = some t)
(hr : rowShiftedLeadingTerm? reducer shift = some r)
(hpos : t.position = r.position)
(hle : r.shiftedDegree ≤ t.shiftedDegree)
:
shiftedEntryDegree? (cancelShiftedLeadingTerm target reducer shift) shift t.position ≠ some t.shiftedDegree
theorem
CompPoly.PolynomialMatrix.cancelShiftedLeadingTerm_entry_bound
{F : Type u_1}
[Field F]
[BEq F]
[LawfulBEq F]
[DecidableEq F]
{target reducer : PolynomialRow F}
{shift : Array ℕ}
{t r : ShiftedLeadingTerm F}
(ht : rowShiftedLeadingTerm? target shift = some t)
(hr : rowShiftedLeadingTerm? reducer shift = some r)
(hpos : t.position = r.position)
(hle : r.shiftedDegree ≤ t.shiftedDegree)
(hsize : Array.size reducer = Array.size target)
{k : ℕ}
(hk : k < Array.size target)
(hne : rowGet (cancelShiftedLeadingTerm target reducer shift) k ≠ 0)
:
(rowGet (cancelShiftedLeadingTerm target reducer shift) k).natDegree + shift.getD k 0 ≤ t.shiftedDegree
theorem
CompPoly.PolynomialMatrix.cancelShiftedLeadingTerm_entry_strict_of_pos_lt
{F : Type u_1}
[Field F]
[BEq F]
[LawfulBEq F]
[DecidableEq F]
{target reducer : PolynomialRow F}
{shift : Array ℕ}
{t r : ShiftedLeadingTerm F}
(ht : rowShiftedLeadingTerm? target shift = some t)
(hr : rowShiftedLeadingTerm? reducer shift = some r)
(hpos : t.position = r.position)
(hle : r.shiftedDegree ≤ t.shiftedDegree)
(hsize : Array.size reducer = Array.size target)
{k : ℕ}
(hk : k < Array.size target)
(hposlt : t.position < k)
(hne : rowGet (cancelShiftedLeadingTerm target reducer shift) k ≠ 0)
:
(rowGet (cancelShiftedLeadingTerm target reducer shift) k).natDegree + shift.getD k 0 < t.shiftedDegree