Polynomial arithmetic with supplied binary-quotient coefficient vectors

def MIPRE.LowDegree.BinaryQuotient.addCoeffLists : List Cost.BitStr → List Cost.BitStr → List Cost.BitStr

Add coefficient lists, keeping unmatched final coefficients.

Equations

• MIPRE.LowDegree.BinaryQuotient.addCoeffLists [] x✝ = x✝
• MIPRE.LowDegree.BinaryQuotient.addCoeffLists (a :: as) [] = a :: as
• MIPRE.LowDegree.BinaryQuotient.addCoeffLists (a :: as) (b :: bs) = MIPRE.LowDegree.BinaryPolynomial.xorBits a b :: MIPRE.LowDegree.BinaryQuotient.addCoeffLists as bs

@[simp]

theorem MIPRE.LowDegree.BinaryQuotient.addCoeffLists_nil_right (as : List Cost.BitStr) : addCoeffLists as [] = as

@[simp]

theorem MIPRE.LowDegree.BinaryQuotient.length_addCoeffLists (as bs : List Cost.BitStr) : (addCoeffLists as bs).length = max as.length bs.length

theorem MIPRE.LowDegree.BinaryQuotient.addCoeffLists_width (as bs : List Cost.BitStr) (n : ℕ) (ha : ∀ a ∈ as, List.length a = n) (hb : ∀ b ∈ bs, List.length b = n) (c : Cost.BitStr) : c ∈ addCoeffLists as bs → List.length c = n

Addition keeps all correctly sized coefficients correctly sized.

theorem MIPRE.LowDegree.BinaryQuotient.addCoeffLists_width_le (as bs : List Cost.BitStr) (n : ℕ) (ha : ∀ a ∈ as, List.length a ≤ n) (hb : ∀ b ∈ bs, List.length b ≤ n) (c : Cost.BitStr) : c ∈ addCoeffLists as bs → List.length c ≤ n

Addition cannot exceed a common bound on the input coefficient widths.

theorem MIPRE.LowDegree.BinaryQuotient.coeffPolynomial_addCoeffLists {R : Type u_1} [CommRing R] [CharP R 2] (z : R) (as bs : List Cost.BitStr) (n : ℕ) (ha : ∀ a ∈ as, List.length a = n) (hb : ∀ b ∈ bs, List.length b = n) : coeffPolynomial z (addCoeffLists as bs) = coeffPolynomial z as + coeffPolynomial z bs

Coefficient-list addition implements addition of the interpreted polynomials.

@[reducible, inline]

abbrev MIPRE.LowDegree.BinaryQuotient.AddState : Type

Equations

• MIPRE.LowDegree.BinaryQuotient.AddState = (List MIPRE.Cost.BitStr × List MIPRE.Cost.BitStr)

def MIPRE.LowDegree.BinaryQuotient.addStep (s : AddState) (a : Cost.BitStr) : AddState

Equations

• MIPRE.LowDegree.BinaryQuotient.addStep s a = match s.1 with | [] => ([], a :: s.2) | b :: bs => (bs, MIPRE.LowDegree.BinaryPolynomial.xorBits a b :: s.2)

def MIPRE.LowDegree.BinaryQuotient.finishAdd (s : AddState) : List Cost.BitStr

Equations

• MIPRE.LowDegree.BinaryQuotient.finishAdd s = s.2.reverse ++ s.1

theorem MIPRE.LowDegree.BinaryQuotient.finishAdd_fold (as bs acc : List Cost.BitStr) : finishAdd (List.foldl addStep (bs, acc) as) = acc.reverse ++ addCoeffLists as bs

noncomputable def MIPRE.LowDegree.BinaryQuotient.addStepProg : Cost.PolyTimeFun (AddState × Cost.BitStr) AddState

Equations

• One or more equations did not get rendered due to their size.

theorem MIPRE.LowDegree.BinaryQuotient.addStepProg_apply (s : AddState) (a : Cost.BitStr) : addStepProg.toFun (s, a) = addStep s a

theorem MIPRE.LowDegree.BinaryQuotient.addStep_growth (s : AddState) (a : Cost.BitStr) : Cost.esize (addStepProg.toFun (s, a)) ≤ Cost.esize s + Polynomial.eval (Cost.esize a) (5 * Polynomial.X + 5)

noncomputable def MIPRE.LowDegree.BinaryQuotient.addCoeffListsProg : Cost.PolyTimeFun (List Cost.BitStr × List Cost.BitStr) (List Cost.BitStr)

One globally polynomial-time coefficient addition program.

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem MIPRE.LowDegree.BinaryQuotient.addCoeffListsProg_apply (as bs : List Cost.BitStr) : addCoeffListsProg.toFun (as, bs) = addCoeffLists as bs

def MIPRE.LowDegree.BinaryQuotient.mulCoeffLists (p : Cost.BitStr) : List Cost.BitStr → List Cost.BitStr → List Cost.BitStr

Horner multiplication of two polynomial coefficient lists.

Equations

• One or more equations did not get rendered due to their size.
• MIPRE.LowDegree.BinaryQuotient.mulCoeffLists p [] x✝ = []

theorem MIPRE.LowDegree.BinaryQuotient.length_mulCoeffLists_le (p : Cost.BitStr) (as bs : List Cost.BitStr) : (mulCoeffLists p as bs).length ≤ as.length + bs.length

Each multiplication output has at most the sum of the input coefficient counts.

theorem MIPRE.LowDegree.BinaryQuotient.mulCoeffLists_width (p : Cost.BitStr) (as bs : List Cost.BitStr) (ha : ∀ a ∈ as, List.length a = List.length p) (c : Cost.BitStr) : c ∈ mulCoeffLists p as bs → List.length c = List.length p

Multiplication preserves valid quotient coefficient widths.

theorem MIPRE.LowDegree.BinaryQuotient.coeffPolynomial_scale {R : Type u_1} [CommRing R] [CharP R 2] (z : R) (p a : Cost.BitStr) (bs : List Cost.BitStr) (hz : z ^ List.length p = BinaryPolynomial.evalBits z p) (ha : List.length a = List.length p) : coeffPolynomial z (List.map (BinaryPolynomial.mulReduce p a) bs) = Polynomial.C (BinaryPolynomial.evalBits z a) * coeffPolynomial z bs

Scalar multiplication has the expected polynomial interpretation.

theorem MIPRE.LowDegree.BinaryQuotient.coeffPolynomial_mulCoeffLists {R : Type u_1} [CommRing R] [CharP R 2] (z : R) (p : Cost.BitStr) (as bs : List Cost.BitStr) (hz : z ^ List.length p = BinaryPolynomial.evalBits z p) (ha : ∀ a ∈ as, List.length a = List.length p) : coeffPolynomial z (mulCoeffLists p as bs) = coeffPolynomial z as * coeffPolynomial z bs

Horner multiplication agrees with multiplication of the interpreted polynomials.

@[reducible, inline]

abbrev MIPRE.LowDegree.BinaryQuotient.MulState : Type

Equations

• MIPRE.LowDegree.BinaryQuotient.MulState = (MIPRE.Cost.BitStr × List MIPRE.Cost.BitStr × List MIPRE.Cost.BitStr)

def MIPRE.LowDegree.BinaryQuotient.mulStep (s : MulState) (a : Cost.BitStr) : MulState

Equations

• One or more equations did not get rendered due to their size.

theorem MIPRE.LowDegree.BinaryQuotient.fold_mulStep_shape (pre : List Cost.BitStr) (p : Cost.BitStr) (bs cs : List Cost.BitStr) : (List.foldl mulStep (p, bs, cs) pre).1 = p ∧ (List.foldl mulStep (p, bs, cs) pre).2.1 = bs ∧ (List.foldl mulStep (p, bs, cs) pre).2.2.length ≤ max bs.length cs.length + pre.length

theorem MIPRE.LowDegree.BinaryQuotient.fold_mulStep_width (pre : List Cost.BitStr) (p : Cost.BitStr) (bs cs : List Cost.BitStr) (N : ℕ) (hp : List.length p ≤ N) (ha : ∀ a ∈ pre, List.length a ≤ N) (hc : ∀ c ∈ cs, List.length c ≤ N) (c : Cost.BitStr) : c ∈ (List.foldl mulStep (p, bs, cs) pre).2.2 → List.length c ≤ N

theorem MIPRE.LowDegree.BinaryQuotient.fold_mulStep_eq (as : List Cost.BitStr) (p : Cost.BitStr) (bs cs : List Cost.BitStr) : List.foldl mulStep (p, bs, cs) as = (p, bs, List.foldl (fun (acc : List Cost.BitStr) (a : Cost.BitStr) => addCoeffLists (List.map (BinaryPolynomial.mulReduce p a) bs) (BinaryPolynomial.zeroBits p :: acc)) cs as)

noncomputable def MIPRE.LowDegree.BinaryQuotient.mulStepProg : Cost.PolyTimeFun (MulState × Cost.BitStr) MulState

Equations

• One or more equations did not get rendered due to their size.

theorem MIPRE.LowDegree.BinaryQuotient.mulStep_bounded : mulStepProg.FoldBounded (20 * Polynomial.X ^ 2 + 20 * Polynomial.X + 20)

noncomputable def MIPRE.LowDegree.BinaryQuotient.mulCoeffListsProg : Cost.PolyTimeFun (Cost.BitStr × List Cost.BitStr × List Cost.BitStr) (List Cost.BitStr)

A globally polynomial-time product of two supplied-quotient coefficient lists.

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem MIPRE.LowDegree.BinaryQuotient.mulCoeffListsProg_apply (p : Cost.BitStr) (as bs : List Cost.BitStr) : mulCoeffListsProg.toFun (p, as, bs) = mulCoeffLists p as bs

theorem MIPRE.LowDegree.BinaryQuotient.mulCoeffLists_width_le (p : Cost.BitStr) (as bs : List Cost.BitStr) (N : ℕ) (hp : List.length p ≤ N) (ha : ∀ a ∈ as, List.length a ≤ N) (c : Cost.BitStr) : c ∈ mulCoeffLists p as bs → List.length c ≤ N

A common width bound for the left coefficients and modulus bounds every product coefficient.