Raw Univariate Polynomial Proofs

Proofs about operations on raw computable univariate polynomials.

theorem CompPoly.CPolynomial.Raw.pow_zero {R : Type u_1} [Semiring R] [BEq R] (p : Raw R) : p ^ 0 = C 1

theorem CompPoly.CPolynomial.Raw.pow_succ {R : Type u_1} [Semiring R] [BEq R] (p : Raw R) (n : ℕ) : p ^ (n + 1) = p * p ^ n

theorem CompPoly.CPolynomial.Raw.matchSize_size_eq {Q : Type u_2} [Semiring Q] {p q : Raw Q} : match Array.matchSize p q 0 with | (p', q') => p'.size = q'.size

theorem CompPoly.CPolynomial.Raw.matchSize_size {Q : Type u_2} [Semiring Q] {p q : Raw Q} : match Array.matchSize p q 0 with | (p', snd) => p'.size = max (Array.size p) (Array.size q)

theorem CompPoly.CPolynomial.Raw.zipWith_size {R : Type u_4} {f : R → R → R} {a b : Array R} (h : a.size = b.size) : (Array.zipWith f a b).size = a.size

theorem CompPoly.CPolynomial.Raw.concat_coeff₁ {R : Type u_1} [Semiring R] (p q : Raw R) (i : ℕ) : i < Array.size p → (p ++ q).coeff i = p.coeff i

theorem CompPoly.CPolynomial.Raw.concat_coeff₂ {R : Type u_1} [Semiring R] (p q : Raw R) (i : ℕ) : i ≥ Array.size p → (p ++ q).coeff i = q.coeff (i - Array.size p)

theorem CompPoly.CPolynomial.Raw.add_size {Q : Type u_2} [Semiring Q] {p q : Raw Q} : Array.size (p.addRaw q) = max (Array.size p) (Array.size q)

theorem CompPoly.CPolynomial.Raw.add_coeff {Q : Type u_2} [Semiring Q] {p q : Raw Q} {i : ℕ} (hi : i < Array.size (p.addRaw q)) : (p.addRaw q)[i] = p.coeff i + q.coeff i

theorem CompPoly.CPolynomial.Raw.add_coeff? {Q : Type u_2} [Semiring Q] (p q : Raw Q) (i : ℕ) : (p.addRaw q).coeff i = p.coeff i + q.coeff i

theorem CompPoly.CPolynomial.Raw.add_coeff_trimmed {R : Type u_1} [Semiring R] [BEq R] [LawfulBEq R] (p q : Raw R) (i : ℕ) : (p + q).coeff i = p.coeff i + q.coeff i

theorem CompPoly.CPolynomial.Raw.add_equiv_raw {R : Type u_1} [Semiring R] [BEq R] [LawfulBEq R] (p q : Raw R) : Trim.equiv (p.add q) (p.addRaw q)

theorem CompPoly.CPolynomial.Raw.smul_equiv {R : Type u_1} [Semiring R] (p : Raw R) (i : ℕ) (r : R) : (smul r p).coeff i = r * p.coeff i

theorem CompPoly.CPolynomial.Raw.nsmulRaw_equiv {R : Type u_1} [Semiring R] [BEq R] (p : Raw R) [LawfulBEq R] (n i : ℕ) : (nsmulRaw n p).trim.coeff i = ↑n * p.trim.coeff i

theorem CompPoly.CPolynomial.Raw.mul_pow_assoc {R : Type u_1} [Semiring R] [BEq R] (p : Raw R) (n : ℕ) (q : Raw R) (m l : ℕ) : l + m = n → p.mul^[n] q = p.mul^[m] (p.mul^[l] q)

theorem CompPoly.CPolynomial.Raw.mul_pow_succ {R : Type u_1} [Semiring R] [BEq R] (p q : Raw R) (n : ℕ) : p.mul^[n + 1] q = p.mul (p.mul^[n] q)

theorem CompPoly.CPolynomial.Raw.trim_add_trim {R : Type u_1} [Semiring R] [BEq R] [LawfulBEq R] (p q : Raw R) : p.trim + q = p + q

@[simp]

theorem CompPoly.CPolynomial.Raw.zero_def {Q : Type u_2} : 0 = #[]

theorem CompPoly.CPolynomial.Raw.add_comm {R : Type u_1} [Semiring R] [BEq R] (p q : Raw R) : p + q = q + p

theorem CompPoly.CPolynomial.Raw.zero_canonical {R : Type u_1} [Semiring R] [BEq R] : trim 0 = 0

theorem CompPoly.CPolynomial.Raw.monomial_canonical {R : Type u_1} [Semiring R] [BEq R] [LawfulBEq R] [DecidableEq R] (n : ℕ) (c : R) : (monomial n c).trim = monomial n c

theorem CompPoly.CPolynomial.Raw.X_canonical {R : Type u_1} [Semiring R] [BEq R] [Nontrivial R] [LawfulBEq R] : X.trim = X

theorem CompPoly.CPolynomial.Raw.coeff_monomial {R : Type u_1} [Semiring R] [DecidableEq R] {n i : ℕ} {c : R} : (monomial n c).coeff i = if n = i then c else 0

theorem CompPoly.CPolynomial.Raw.coeff_C {R : Type u_1} [Semiring R] (r : R) (i : ℕ) : (C r).coeff i = if i = 0 then r else 0

theorem CompPoly.CPolynomial.Raw.coeff_X {R : Type u_1} [Semiring R] (i : ℕ) : X.coeff i = if i = 1 then 1 else 0

@[simp]

theorem CompPoly.CPolynomial.Raw.coeff_zero {R : Type u_1} [Semiring R] (i : ℕ) : coeff 0 i = 0

theorem CompPoly.CPolynomial.Raw.coeff_one {R : Type u_1} [Semiring R] (i : ℕ) : coeff 1 i = if i = 0 then 1 else 0

theorem CompPoly.CPolynomial.Raw.zero_add {R : Type u_1} [Semiring R] [BEq R] (p : Raw R) (hp : p.canonical) : 0 + p = p

theorem CompPoly.CPolynomial.Raw.add_zero {R : Type u_1} [Semiring R] [BEq R] (p : Raw R) (hp : p.canonical) : p + 0 = p

theorem CompPoly.CPolynomial.Raw.zero_add_trim {R : Type u_1} [Semiring R] [BEq R] [LawfulBEq R] (p : Raw R) : 0 + p = p.trim

theorem CompPoly.CPolynomial.Raw.add_zero_trim {R : Type u_1} [Semiring R] [BEq R] [LawfulBEq R] (p : Raw R) : p + 0 = p.trim

theorem CompPoly.CPolynomial.Raw.add_assoc {R : Type u_1} [Semiring R] [BEq R] (p q r : Raw R) [LawfulBEq R] : p + q + r = p + (q + r)

theorem CompPoly.CPolynomial.Raw.foldl_preserves_canonical {R : Type u_1} [Semiring R] [BEq R] {α : Type u_4} (f : Raw R → α → Raw R) (z : Raw R) (as : Array α) (hz : z.trim = z) (hf : ∀ (acc : Raw R) (x : α), (f acc x).trim = f acc x) : (Array.foldl f z as).trim = Array.foldl f z as

theorem CompPoly.CPolynomial.Raw.coeff_foldl_add {R : Type u_1} [Semiring R] [BEq R] {α : Type u_4} [LawfulBEq R] (l : List α) (f : α → Raw R) (z : Raw R) (k : ℕ) : (List.foldl (fun (acc : Raw R) (x : α) => acc + f x) z l).coeff k = z.coeff k + (List.map (fun (x : α) => (f x).coeff k) l).sum

theorem CompPoly.CPolynomial.Raw.sum_zipIdx_eq_sum_range {R : Type u_1} [Semiring R] {α : Type u_4} [AddCommMonoid α] (p : Raw R) (f : R → ℕ → α) : (List.map (fun (x : R × ℕ) => match x with | (a, i) => f a i) (Array.zipIdx p).toList).sum = ∑ i ∈ Finset.range (Array.size p), f (p.coeff i) i

theorem CompPoly.CPolynomial.Raw.double_sum_eq {R : Type u_1} [Semiring R] [BEq R] [LawfulBEq R] (p q r : Raw R) (n : ℕ) : ∑ j ∈ Finset.range (n + 1), ∑ i ∈ Finset.range (j + 1), p.coeff i * q.coeff (j - i) * r.coeff (n - j) = ∑ i ∈ Finset.range (n + 1), ∑ k ∈ Finset.range (n - i + 1), p.coeff i * q.coeff k * r.coeff (n - i - k)

theorem CompPoly.CPolynomial.Raw.sum_range_extend {R : Type u_1} [Semiring R] (p q : Raw R) (k : ℕ) : (∑ i ∈ Finset.range (Array.size p), if k < i then 0 else p.coeff i * q.coeff (k - i)) = ∑ i ∈ Finset.range (k + 1), p.coeff i * q.coeff (k - i)

theorem CompPoly.CPolynomial.Raw.sum_range_reverse {R : Type u_1} [Semiring R] [BEq R] [LawfulBEq R] (p q : Raw R) (k : ℕ) : ∑ i ∈ Finset.range (k + 1), p.coeff i * q.coeff (k - i) = ∑ j ∈ Finset.range (k + 1), p.coeff (k - j) * q.coeff j

theorem CompPoly.CPolynomial.Raw.nsmul_zero {R : Type u_1} [Semiring R] [BEq R] [LawfulBEq R] (p : Raw R) : nsmul 0 p = 0

theorem CompPoly.CPolynomial.Raw.nsmulRawSucc {Q : Type u_2} [Semiring Q] (n : ℕ) (p : Raw Q) : nsmulRaw (n + 1) p = (nsmulRaw n p).addRaw p

theorem CompPoly.CPolynomial.Raw.nsmul_succ {R : Type u_1} [Semiring R] [BEq R] [LawfulBEq R] (n : ℕ) {p : Raw R} : nsmul (n + 1) p = nsmul n p + p

theorem CompPoly.CPolynomial.Raw.smul_coeff {R : Type u_1} [Semiring R] [BEq R] [LawfulBEq R] (a : R) (p : Raw R) (k : ℕ) : (smul a p).coeff k = a * p.coeff k

theorem CompPoly.CPolynomial.Raw.smul_addRaw_distrib {R : Type u_1} [Semiring R] [BEq R] [LawfulBEq R] (a' : R) (q r : Raw R) : smul a' (q.addRaw r) = (smul a' q).addRaw (smul a' r)

theorem CompPoly.CPolynomial.Raw.smul_distrib_trim {R : Type u_1} [Semiring R] [BEq R] [LawfulBEq R] (a' : R) (q r : Raw R) : (smul a' (q + r)).trim = smul a' q + smul a' r

theorem CompPoly.CPolynomial.Raw.coeff_smul_add_distrib {R : Type u_1} [Semiring R] [BEq R] [LawfulBEq R] (a : R) (q r : Raw R) (i : ℕ) : (smul a (q + r)).coeff i = (smul a q).coeff i + (smul a r).coeff i

theorem CompPoly.CPolynomial.Raw.coeff_add_smul {R : Type u_1} [Semiring R] [BEq R] [LawfulBEq R] (a b : R) (q : Raw R) (k : ℕ) : (smul (a + b) q).coeff k = (smul a q).coeff k + (smul b q).coeff k

theorem CompPoly.CPolynomial.Raw.coeff_sum {R : Type u_1} [Semiring R] (p : Raw R) (k : ℕ) : (Array.map (fun (x : R × ℕ) => match x with | (a, i) => (mulPowX i (smul a 1)).coeff k) (Array.zipIdx p)).sum = p.coeff k

theorem CompPoly.CPolynomial.Raw.coeff_mul {R : Type u_1} [Semiring R] [BEq R] [LawfulBEq R] (p q : Raw R) (k : ℕ) : (p * q).coeff k = (List.map (fun (x : R × ℕ) => match x with | (a, i) => (mulPowX i (smul a q)).coeff k) (Array.zipIdx p).toList).sum

theorem CompPoly.CPolynomial.Raw.coeff_mulPowX {R : Type u_1} [Semiring R] [BEq R] [LawfulBEq R] (i : ℕ) (p : Raw R) (k : ℕ) : (mulPowX i p).coeff k = if k < i then 0 else p.coeff (k - i)

theorem CompPoly.CPolynomial.Raw.coeff_mulPowX' {R : Type u_1} [Semiring R] [BEq R] [LawfulBEq R] (p : Raw R) (n i : ℕ) : (mulPowX n p).coeff i = if i < n then 0 else p.coeff (i - n)

theorem CompPoly.CPolynomial.Raw.mulPowX_coeff' {R : Type u_1} [Semiring R] [BEq R] [LawfulBEq R] (p : Raw R) (n k : ℕ) : (mulPowX n p).coeff k = if k < n then 0 else p.coeff (k - n)

theorem CompPoly.CPolynomial.Raw.coeff_mulPowX_smul_add {R : Type u_1} [Semiring R] [BEq R] [LawfulBEq R] (i : ℕ) (a b : R) (q : Raw R) (k : ℕ) : (mulPowX i (smul (a + b) q)).coeff k = (mulPowX i (smul a q)).coeff k + (mulPowX i (smul b q)).coeff k

theorem CompPoly.CPolynomial.Raw.mulPowX_zero {R : Type u_1} [Semiring R] (p : Raw R) : mulPowX 0 p = p

theorem CompPoly.CPolynomial.Raw.equiv_mul_one {R : Type u_1} [Semiring R] [BEq R] [LawfulBEq R] (p : Raw R) : Trim.equiv (p * 1) p

theorem CompPoly.CPolynomial.Raw.mul_is_trimmed {R : Type u_1} [Semiring R] [BEq R] [LawfulBEq R] (p q : Raw R) : (p * q).trim = p * q

theorem CompPoly.CPolynomial.Raw.coeff_mul_eq_sum_range {R : Type u_1} [Semiring R] [BEq R] [LawfulBEq R] (p q : Raw R) (k n : ℕ) (h : Array.size p ≤ n) : (p * q).coeff k = (List.map (fun (i : ℕ) => (mulPowX i (smul (p.coeff i) q)).coeff k) (List.range n)).sum

theorem CompPoly.CPolynomial.Raw.mul_eq_foldl {R : Type u_1} [Semiring R] [BEq R] (p q : Raw R) : p * q = Array.foldl (fun (acc : Raw R) (x : R × ℕ) => match x with | (a, i) => acc + mulPowX i (smul a q)) (mk #[]) (Array.zipIdx p)

theorem CompPoly.CPolynomial.Raw.C_mul_eq_smul_trim {R : Type u_1} [Semiring R] [BEq R] [LawfulBEq R] (r : R) (q : Raw R) : C r * q = (smul r q).trim

theorem CompPoly.CPolynomial.Raw.smul_one_eq_self {R : Type u_1} [Semiring R] (p : Raw R) : smul 1 p = p

theorem CompPoly.CPolynomial.Raw.smul_zero_eq_replicate_zero {R : Type u_1} [Semiring R] (p : Raw R) : smul 0 p = mk (Array.replicate (Array.size p) 0)

theorem CompPoly.CPolynomial.Raw.trim_replicate_zero {R : Type u_1} [Semiring R] [BEq R] [LawfulBEq R] (n : ℕ) : (mk (Array.replicate n 0)).trim = 0

theorem CompPoly.CPolynomial.Raw.smul_zero_trim {R : Type u_1} [Semiring R] [BEq R] [LawfulBEq R] (p : Raw R) : (smul 0 p).trim = 0

theorem CompPoly.CPolynomial.Raw.X_mul_eq_mulX_trim {R : Type u_1} [Semiring R] [BEq R] [LawfulBEq R] (p : Raw R) : X * p = p.mulX.trim

theorem CompPoly.CPolynomial.Raw.mulX_monomial_one {R : Type u_1} [Semiring R] [BEq R] [DecidableEq R] [LawfulBEq R] [Nontrivial R] (n : ℕ) : (monomial n 1).mulX = monomial (n + 1) 1

theorem CompPoly.CPolynomial.Raw.X_pow_eq_monomial_one {R : Type u_1} [Semiring R] [BEq R] [DecidableEq R] [LawfulBEq R] [Nontrivial R] (n : ℕ) : X ^ n = monomial n 1

theorem CompPoly.CPolynomial.Raw.smul_monomial_one_trim {R : Type u_1} [Semiring R] [BEq R] [DecidableEq R] [LawfulBEq R] [Nontrivial R] (n : ℕ) (r : R) : (smul r (monomial n 1)).trim = monomial n r

theorem CompPoly.CPolynomial.Raw.smul_mulPowX_coeff {R : Type u_1} [Semiring R] [BEq R] [LawfulBEq R] (a : R) (q : Raw R) (i k : ℕ) : (mulPowX i (smul a q)).coeff k = if k < i then 0 else a * q.coeff (k - i)

theorem CompPoly.CPolynomial.Raw.mul_coeff_list {R : Type u_1} [Semiring R] [BEq R] [LawfulBEq R] (p q : Raw R) (k : ℕ) : (p * q).coeff k = (List.map (fun (x : R × ℕ) => match x with | (a, i) => if k < i then 0 else a * q.coeff (k - i)) (Array.zipIdx p).toList).sum

theorem CompPoly.CPolynomial.Raw.mul_coeff_range_size {R : Type u_1} [Semiring R] [BEq R] [LawfulBEq R] (p q : Raw R) (k : ℕ) : (p * q).coeff k = ∑ i ∈ Finset.range (Array.size p), if k < i then 0 else p.coeff i * q.coeff (k - i)

theorem CompPoly.CPolynomial.Raw.mul_coeff {R : Type u_1} [Semiring R] [BEq R] [LawfulBEq R] (p q : Raw R) (k : ℕ) : (p * q).coeff k = ∑ i ∈ Finset.range (k + 1), p.coeff i * q.coeff (k - i)

theorem CompPoly.CPolynomial.Raw.mul_assoc_coeff_rhs {R : Type u_1} [Semiring R] [BEq R] [LawfulBEq R] (p q r : Raw R) (n : ℕ) : (p * (q * r)).coeff n = ∑ i ∈ Finset.range (n + 1), ∑ j ∈ Finset.range (n - i + 1), p.coeff i * q.coeff j * r.coeff (n - i - j)

theorem CompPoly.CPolynomial.Raw.mul_mul_coeff {R : Type u_1} [Semiring R] [BEq R] [LawfulBEq R] (p q r : Raw R) (n : ℕ) : (p * q * r).coeff n = ∑ j ∈ Finset.range (n + 1), ∑ i ∈ Finset.range (j + 1), p.coeff i * q.coeff (j - i) * r.coeff (n - j)

theorem CompPoly.CPolynomial.Raw.mul_assoc_coeff {R : Type u_1} [Semiring R] [BEq R] [LawfulBEq R] (p q r : Raw R) (n : ℕ) : (p * q * r).coeff n = (p * (q * r)).coeff n

theorem CompPoly.CPolynomial.Raw.mul_assoc_equiv {R : Type u_1} [Semiring R] [BEq R] [LawfulBEq R] (p q r : Raw R) : Trim.equiv (p * q * r) (p * (q * r))

theorem CompPoly.CPolynomial.Raw.mul_zero {R : Type u_1} [Semiring R] [BEq R] [LawfulBEq R] (p : Raw R) : p * 0 = 0

theorem CompPoly.CPolynomial.Raw.zero_mul {R : Type u_1} [Semiring R] [BEq R] [LawfulBEq R] (p : Raw R) : 0 * p = 0

theorem CompPoly.CPolynomial.Raw.mul_one_trim {R : Type u_1} [Semiring R] [BEq R] [LawfulBEq R] (p : Raw R) : p * 1 = p.trim

theorem CompPoly.CPolynomial.Raw.one_mul_trim {R : Type u_1} [Semiring R] [BEq R] [LawfulBEq R] (p : Raw R) : 1 * p = p.trim

theorem CompPoly.CPolynomial.Raw.mul_add {R : Type u_1} [Semiring R] [BEq R] [LawfulBEq R] (p q r : Raw R) : p * (q + r) = p * q + p * r

theorem CompPoly.CPolynomial.Raw.add_mul {R : Type u_1} [Semiring R] [BEq R] [LawfulBEq R] (p q r : Raw R) : (p + q) * r = p * r + q * r

theorem CompPoly.CPolynomial.Raw.mul_assoc {R : Type u_1} [Semiring R] [BEq R] [LawfulBEq R] (p q r : Raw R) : p * q * r = p * (q * r)

theorem CompPoly.CPolynomial.Raw.mul_coeff_comm {R : Type u_1} [CommSemiring R] [BEq R] [LawfulBEq R] (p q : Raw R) (k : ℕ) : ∑ i ∈ Finset.range (k + 1), p.coeff i * q.coeff (k - i) = ∑ i ∈ Finset.range (k + 1), q.coeff i * p.coeff (k - i)

theorem CompPoly.CPolynomial.Raw.mul_comm_coeff {R : Type u_1} [CommSemiring R] [BEq R] [LawfulBEq R] (p q : Raw R) (k : ℕ) : (p * q).coeff k = (q * p).coeff k

theorem CompPoly.CPolynomial.Raw.mul_comm_equiv {R : Type u_1} [CommSemiring R] [BEq R] [LawfulBEq R] (p q : Raw R) : Trim.equiv (p * q) (q * p)

theorem CompPoly.CPolynomial.Raw.mul_comm {R : Type u_1} [CommSemiring R] [BEq R] [LawfulBEq R] (p q : Raw R) : p * q = q * p

theorem CompPoly.CPolynomial.Raw.neg_coeff {R : Type u_3} [NegZeroClass R] (p : Raw R) (i : ℕ) : p.neg.coeff i = -p.coeff i

theorem CompPoly.CPolynomial.Raw.neg_trim {R : Type u_1} [Ring R] [BEq R] [LawfulBEq R] (p : Raw R) : p.trim = p → (-p).trim = -p

theorem CompPoly.CPolynomial.Raw.neg_add_cancel {R : Type u_1} [Ring R] [BEq R] [LawfulBEq R] (p : Raw R) : -p + p = 0

theorem CompPoly.CPolynomial.Raw.sub_coeff {R : Type u_1} [Ring R] [BEq R] [LawfulBEq R] (p q : Raw R) (i : ℕ) : (p - q).coeff i = p.coeff i - q.coeff i

@[implicit_reducible]

instance CompPoly.CPolynomial.Raw.instAddCommSemigroupOfLawfulBEq {R : Type u_1} [Semiring R] [BEq R] [LawfulBEq R] : AddCommSemigroup (Raw R)

theorem CompPoly.CPolynomial.Raw.pow_is_trimmed {R : Type u_1} [Semiring R] [BEq R] [LawfulBEq R] [Nontrivial R] (p : Raw R) (n : ℕ) : (p ^ n).trim = p ^ n

pow preserves trimming (Raw-level version).

theorem CompPoly.CPolynomial.Raw.pow_add {R : Type u_1} [Semiring R] [BEq R] [LawfulBEq R] [Nontrivial R] (p : Raw R) (a b : ℕ) : p ^ (a + b) = p ^ a * p ^ b

Additive law for exponentiation: $ p ^ {a + b} = p ^ a \cdot p ^ b $.

@[irreducible]

theorem CompPoly.CPolynomial.Raw.powBySq_eq_pow {R : Type u_1} [Semiring R] [BEq R] [LawfulBEq R] [Nontrivial R] (p : Raw R) (n : ℕ) : p.powBySq n = p ^ n

powBySq agrees with pow (repeated squaring = repeated multiplication).