Lee-O'Sullivan Row-Span Transport Helpers

Transport between executable polynomial rows and semantic bivariate span combinations.

theorem CompPoly.GuruswamiSudan.LeeOSullivan.coeff_ofCoeffRow_rowLinearCombination_lee_of_lt {F : Type u_1} [Field F] [BEq F] [LawfulBEq F] [DecidableEq F] (R G : CPolynomial F) (params : GSInterpParams) (coeffs : Array (CPolynomial F)) {k j : ℕ} (hj : j < leeOSullivanWidth params) : (CBivariate.ofCoeffRow (PolynomialMatrix.rowLinearCombination coeffs (leeOSullivanBasisRowsWithRG R G params))).coeff k j = (koetterBasisCombination (fun (i : ℕ) => coeffs.getD i 0) (leeOSullivanBasisPolynomials R G params)).coeff k j

Within the Lee row width, a row-linear combination of executable Lee rows has the same coefficients as the corresponding bivariate basis combination.

theorem CompPoly.GuruswamiSudan.LeeOSullivan.leeOSullivanBasisPolynomial_coeff_eq_zero_of_width_le {F : Type u_1} [Field F] [BEq F] [LawfulBEq F] [DecidableEq F] (R G : CPolynomial F) (params : GSInterpParams) {idx x j : ℕ} (hidx : idx < leeOSullivanWidth params) (hj : leeOSullivanWidth params ≤ j) : (leeOSullivanBasisPolynomial R G params idx).coeff x j = 0

Lee basis polynomials are bounded by the Lee row width in Y.

theorem CompPoly.GuruswamiSudan.LeeOSullivan.coeff_koetterBasisCombination_lee_eq_zero_of_width_le {F : Type u_1} [Field F] [BEq F] [LawfulBEq F] [DecidableEq F] (R G : CPolynomial F) (params : GSInterpParams) (weights : ℕ → CPolynomial F) {x j : ℕ} (hj : leeOSullivanWidth params ≤ j) : (koetterBasisCombination weights (leeOSullivanBasisPolynomials R G params)).coeff x j = 0

Bivariate combinations of Lee basis polynomials are bounded by the Lee row width in Y.

theorem CompPoly.GuruswamiSudan.LeeOSullivan.ofCoeffRow_rowLinearCombination_lee_eq_combination {F : Type u_1} [Field F] [BEq F] [LawfulBEq F] [DecidableEq F] (R G : CPolynomial F) (params : GSInterpParams) (coeffs : Array (CPolynomial F)) : CBivariate.ofCoeffRow (PolynomialMatrix.rowLinearCombination coeffs (leeOSullivanBasisRowsWithRG R G params)) = koetterBasisCombination (fun (i : ℕ) => coeffs.getD i 0) (leeOSullivanBasisPolynomials R G params)

A polynomial-row linear combination of the executable Lee rows represents the same bivariate polynomial as the corresponding Lee basis combination.

theorem CompPoly.GuruswamiSudan.LeeOSullivan.ofCoeffRow_rowSpan_lee_spanContains {F : Type u_1} [Field F] [BEq F] [LawfulBEq F] [DecidableEq F] (R G : CPolynomial F) (params : GSInterpParams) {row : PolynomialRow F} (hrow : row ∈ (leeOSullivanBasisRowsWithRG R G params).RowSpan) : koetterBasisSpanContains (leeOSullivanBasisPolynomials R G params) (CBivariate.ofCoeffRow row)

A row in the executable Lee row span represents a bivariate polynomial in the corresponding Lee basis span.

theorem CompPoly.GuruswamiSudan.LeeOSullivan.koetterBasisCombination_add_weights {F : Type u_1} [Field F] [BEq F] [LawfulBEq F] [DecidableEq F] (weights₁ weights₂ : ℕ → CPolynomial F) (basis : Array (CBivariate F)) : koetterBasisCombination (fun (idx : ℕ) => weights₁ idx + weights₂ idx) basis = koetterBasisCombination weights₁ basis + koetterBasisCombination weights₂ basis

theorem CompPoly.GuruswamiSudan.LeeOSullivan.koetterBasisCombination_neg_weights {F : Type u_1} [Field F] [BEq F] [LawfulBEq F] [DecidableEq F] (weights : ℕ → CPolynomial F) (basis : Array (CBivariate F)) : koetterBasisCombination (fun (idx : ℕ) => -weights idx) basis = -koetterBasisCombination weights basis

theorem CompPoly.GuruswamiSudan.LeeOSullivan.koetterBasisSpanContains_add {F : Type u_1} [Field F] [BEq F] [LawfulBEq F] [DecidableEq F] {basis : Array (CBivariate F)} {P Q : CBivariate F} (hP : koetterBasisSpanContains basis P) (hQ : koetterBasisSpanContains basis Q) : koetterBasisSpanContains basis (P + Q)

theorem CompPoly.GuruswamiSudan.LeeOSullivan.koetterBasisSpanContains_neg {F : Type u_1} [Field F] [BEq F] [LawfulBEq F] [DecidableEq F] {basis : Array (CBivariate F)} {P : CBivariate F} (hP : koetterBasisSpanContains basis P) : koetterBasisSpanContains basis (-P)

theorem CompPoly.GuruswamiSudan.LeeOSullivan.koetterBasisSpanContains_sub {F : Type u_1} [Field F] [BEq F] [LawfulBEq F] [DecidableEq F] {basis : Array (CBivariate F)} {P Q : CBivariate F} (hP : koetterBasisSpanContains basis P) (hQ : koetterBasisSpanContains basis Q) : koetterBasisSpanContains basis (P - Q)

theorem CompPoly.GuruswamiSudan.LeeOSullivan.koetterBasisCombination_single_weight {F : Type u_1} [Field F] [BEq F] [LawfulBEq F] [DecidableEq F] (basis : Array (CBivariate F)) {idx : ℕ} (hidx : idx < basis.size) (weight : CPolynomial F) : koetterBasisCombination (fun (j : ℕ) => if (j == idx) = true then weight else 0) basis = CBivariate.ofYConstant weight * basis.getD idx 0

theorem CompPoly.GuruswamiSudan.LeeOSullivan.koetterBasisSpanContains_single {F : Type u_1} [Field F] [BEq F] [LawfulBEq F] [DecidableEq F] (basis : Array (CBivariate F)) {idx : ℕ} (hidx : idx < basis.size) (weight : CPolynomial F) : koetterBasisSpanContains basis (CBivariate.ofYConstant weight * basis.getD idx 0)

theorem CompPoly.GuruswamiSudan.LeeOSullivan.koetterBasisCombination_congr_weights {F : Type u_1} [Field F] [BEq F] [LawfulBEq F] [DecidableEq F] {basis : Array (CBivariate F)} {weights₁ weights₂ : ℕ → CPolynomial F} (hweights : ∀ idx < basis.size, weights₁ idx = weights₂ idx) : koetterBasisCombination weights₁ basis = koetterBasisCombination weights₂ basis

theorem CompPoly.GuruswamiSudan.LeeOSullivan.ofCoeffRow_toCoeffRow_eq_of_width_le {F : Type u_1} [Field F] [BEq F] [LawfulBEq F] {width : ℕ} {Q : CBivariate F} (hY : ∀ (i j : ℕ), width ≤ j → Q.coeff i j = 0) : CBivariate.ofCoeffRow (CBivariate.toCoeffRow width Q) = Q

theorem CompPoly.GuruswamiSudan.LeeOSullivan.ofCoeffRow_lee_rowSpan_of_spanContains {F : Type u_1} [Field F] [BEq F] [LawfulBEq F] [DecidableEq F] (R G : CPolynomial F) (params : GSInterpParams) {Q : CBivariate F} (hspan : koetterBasisSpanContains (leeOSullivanBasisPolynomials R G params) Q) : ∃ row ∈ (leeOSullivanBasisRowsWithRG R G params).RowSpan, CBivariate.ofCoeffRow row = Q

theorem CompPoly.GuruswamiSudan.LeeOSullivan.coeff_ofCoeffRow_rowGet {F : Type u_1} [Field F] [BEq F] [LawfulBEq F] (row : PolynomialRow F) (i j : ℕ) : (CBivariate.ofCoeffRow row).coeff i j = (PolynomialMatrix.rowGet row j).coeff i

theorem CompPoly.GuruswamiSudan.LeeOSullivan.ofCoeffRow_matrix_getD_semantic_rowSpan {F : Type u_1} [Field F] [BEq F] [LawfulBEq F] (M : PolynomialMatrix F) {i : ℕ} (hi : i < Array.size M) : ∃ spanRow ∈ M.RowSpan, CBivariate.ofCoeffRow spanRow = CBivariate.ofCoeffRow (Array.getD M i #[])

theorem CompPoly.GuruswamiSudan.LeeOSullivan.ofCoeffRow_eq_zero_of_rowShiftedDegree?_none {F : Type u_1} [Field F] [BEq F] [LawfulBEq F] {row : PolynomialRow F} {shift : Array ℕ} (hdeg : PolynomialMatrix.rowShiftedDegree? row shift = none) : CBivariate.ofCoeffRow row = 0

theorem CompPoly.GuruswamiSudan.LeeOSullivan.rowSpan_lee_row_size {F : Type u_1} [Field F] [BEq F] [LawfulBEq F] [DecidableEq F] (R G : CPolynomial F) (params : GSInterpParams) {row : PolynomialRow F} (hrow : row ∈ (leeOSullivanBasisRowsWithRG R G params).RowSpan) : Array.size row = leeOSullivanWidth params

theorem CompPoly.GuruswamiSudan.LeeOSullivan.ofCoeffRow_rowSpan_lee_coeff_eq_zero_of_width_le {F : Type u_1} [Field F] [BEq F] [LawfulBEq F] [DecidableEq F] (R G : CPolynomial F) (params : GSInterpParams) {row : PolynomialRow F} (hrow : row ∈ (leeOSullivanBasisRowsWithRG R G params).RowSpan) {i j : ℕ} (hj : leeOSullivanWidth params ≤ j) : (CBivariate.ofCoeffRow row).coeff i j = 0

theorem CompPoly.GuruswamiSudan.LeeOSullivan.natWeightedDegree_ofCoeffRow_le_of_lee_rowShiftedDegree?_le {F : Type u_1} [Field F] [BEq F] [LawfulBEq F] (params : GSInterpParams) (row : PolynomialRow F) {degree : ℕ} (hdeg : PolynomialMatrix.rowShiftedDegree? row (leeOSullivanShifts params) = some degree) (hle : degree ≤ params.weightedDegreeBound) (hYBound : ∀ (i j : ℕ), leeOSullivanWidth params ≤ j → (CBivariate.ofCoeffRow row).coeff i j = 0) : (CBivariate.ofCoeffRow row).natWeightedDegree 1 (yWeight params) ≤ params.weightedDegreeBound

theorem CompPoly.GuruswamiSudan.LeeOSullivan.ofCoeffRow_ne_zero_of_rowShiftedDegree?_some {F : Type u_1} [Field F] [BEq F] [LawfulBEq F] {row : PolynomialRow F} {shift : Array ℕ} {degree : ℕ} (hdeg : PolynomialMatrix.rowShiftedDegree? row shift = some degree) : CBivariate.ofCoeffRow row ≠ 0

theorem CompPoly.GuruswamiSudan.LeeOSullivan.hasMultiplicityAtLeast_koetterBasisCombination {F : Type u_1} [Field F] [BEq F] [LawfulBEq F] [DecidableEq F] (weights : ℕ → CPolynomial F) (basis : Array (CBivariate F)) {x y : F} {m : ℕ} (hbasis : ∀ idx < basis.size, (basis.getD idx 0).HasMultiplicityAtLeast x y m) : (koetterBasisCombination weights basis).HasMultiplicityAtLeast x y m

A Y-constant linear combination of basis entries satisfying a pointwise multiplicity constraint satisfies that constraint.

theorem CompPoly.GuruswamiSudan.LeeOSullivan.koetterBasisCombination_satisfiesMultiplicityConstraints {F : Type u_1} [Field F] [BEq F] [LawfulBEq F] [DecidableEq F] (weights : ℕ → CPolynomial F) (basis : Array (CBivariate F)) {points : Array (F × F)} {m : ℕ} (hbasis : ∀ idx < basis.size, (basis.getD idx 0).SatisfiesMultiplicityConstraints points m) : (koetterBasisCombination weights basis).SatisfiesMultiplicityConstraints points m

A Y-constant linear combination of basis entries satisfying all packed multiplicity constraints satisfies the same packed constraints.

theorem CompPoly.GuruswamiSudan.LeeOSullivan.ofCoeffRow_rowSpan_lee_satisfiesMultiplicityConstraints {F : Type u_1} [Field F] [BEq F] [LawfulBEq F] [DecidableEq F] (R G : CPolynomial F) (params : GSInterpParams) {points : Array (F × F)} {row : PolynomialRow F} (hbasis : ∀ idx < (leeOSullivanBasisPolynomials R G params).size, ((leeOSullivanBasisPolynomials R G params).getD idx 0).SatisfiesMultiplicityConstraints points params.multiplicity) (hrow : row ∈ (leeOSullivanBasisRowsWithRG R G params).RowSpan) : (CBivariate.ofCoeffRow row).SatisfiesMultiplicityConstraints points params.multiplicity

Any executable row in the Lee row span represents a bivariate polynomial satisfying the packed multiplicity constraints, provided every Lee basis entry does.