Shifted Substitution Lemmas

Semantic proof surface for the generic shifted substitution. The executable operation is available independently of these heavier algebraic facts.

theorem CompPoly.GuruswamiSudan.shiftedSubstitutionCoeffTerm_sum {F : Type u_1} [Field F] [BEq F] [LawfulBEq F] [DecidableEq F] (coeffY f g : CPolynomial F) (t y : ℕ) : List.foldl (fun (acc : CPolynomial F) (r : ℕ) => acc + shiftedSubstitutionCoeffTerm coeffY f t y r * g ^ r) 0 (List.range (y + 1)) = coeffY * (f + CPolynomial.X ^ t * g) ^ y

The univariate coefficient sum produced by one Y-coefficient in shifted substitution composes to the corresponding binomial expansion.

theorem CompPoly.GuruswamiSudan.composeY_shiftedSubstitutionCoeffFold {F : Type u_1} [Field F] [BEq F] [LawfulBEq F] [DecidableEq F] (coeffY f g : CPolynomial F) (t y : ℕ) : (List.foldl (fun (out : CBivariate F) (r : ℕ) => have contribution := CPolynomial.monomial r (shiftedSubstitutionCoeffTerm coeffY f t y r); out + contribution) 0 (List.range (y + 1))).composeY g = List.foldl (fun (acc : CPolynomial F) (r : ℕ) => acc + shiftedSubstitutionCoeffTerm coeffY f t y r * g ^ r) 0 (List.range (y + 1))

Composing the bivariate contribution from one Y-coefficient gives the corresponding univariate shifted-substitution term.

theorem CompPoly.GuruswamiSudan.composeY_substituteYPolynomialPlusXPowerY {F : Type u_1} [Field F] [BEq F] [LawfulBEq F] [DecidableEq F] (Q : CBivariate F) (f g : CPolynomial F) (t : ℕ) : (substituteYPolynomialPlusXPowerY Q f t).composeY g = Q.composeY (f + CPolynomial.X ^ t * g)

Semantic correctness of the shifted substitution Y = f(X) + X^t Y.