Lee-O'Sullivan Row Selection Helpers #
Correctness facts for the least-shifted-degree row scan used by the executable backend.
def
CompPoly.GuruswamiSudan.LeeOSullivan.RowChoiceValid
{F : Type u_1}
[Field F]
[BEq F]
(M : PolynomialMatrix F)
(shift : Array ℕ)
(choice : RowChoice F)
:
Instances For
theorem
CompPoly.GuruswamiSudan.LeeOSullivan.leastShiftedDegreeChoice?_some_valid
{F : Type u_1}
[Field F]
[BEq F]
{M : PolynomialMatrix F}
{shift : Array ℕ}
{choice : RowChoice F}
(hchoice : leastShiftedDegreeChoice? M shift = some choice)
:
RowChoiceValid M shift choice
theorem
CompPoly.GuruswamiSudan.LeeOSullivan.leastShiftedDegreeChoice?_degree_le
{F : Type u_1}
[Field F]
[BEq F]
{M : PolynomialMatrix F}
{shift : Array ℕ}
{choice : RowChoice F}
{i d : ℕ}
(hchoice : leastShiftedDegreeChoice? M shift = some choice)
(hi : i < Array.size M)
(hdeg : PolynomialMatrix.rowShiftedDegree? (Array.getD M i #[]) shift = some d)
:
theorem
CompPoly.GuruswamiSudan.LeeOSullivan.leastShiftedDegreeChoice?_some_of_degree
{F : Type u_1}
[Field F]
[BEq F]
{M : PolynomialMatrix F}
{shift : Array ℕ}
{i d : ℕ}
(hi : i < Array.size M)
(hdeg : PolynomialMatrix.rowShiftedDegree? (Array.getD M i #[]) shift = some d)
:
theorem
CompPoly.GuruswamiSudan.LeeOSullivan.leastShiftedDegreeRow?_some_valid
{F : Type u_1}
[Field F]
[BEq F]
{M : PolynomialMatrix F}
{shift : Array ℕ}
{row : PolynomialRow F}
(hrow : leastShiftedDegreeRow? M shift = some row)
:
∃ (choice : RowChoice F),
leastShiftedDegreeChoice? M shift = some choice ∧ RowChoiceValid M shift choice ∧ choice.row = row