Browse chapters

Imports

import CLRSLean.FourthEdition.Chapter_30.Section_30_1_Representing_Polynomials.S1_CoefficientVectors
import CLRSLean.FourthEdition.Chapter_30.Section_30_1_Representing_Polynomials.S2_PointValueInterpolation
import CLRSLean.FourthEdition.Chapter_30.Section_30_1_Representing_Polynomials.S3_RepresentationOperations

30.1. Representing Polynomials

Fixed-capacity coefficient vectors are connected to Polynomial by exact round trips, and hornerEval_correct verifies their canonical Horner execution. Distinct point-value samples determine bounded-degree polynomials through interpolate_pointValues_roundTrip. Vector addition, pointwise multiplication, and the explicit pair-traversing schoolbook execution have representation theorems and execution-attached exact costs.

Roots of unity and Fourier transforms belong to Section 30.2.

Implementation pages:

              namespace CLRSnamespace Chapter30end Chapter30end CLRS

Definitions and proofs

CLRSLean.FourthEdition.Chapter_30.Section_30_1_Representing_Polynomials.S1_CoefficientVectors

Chapter 30.1: Fixed-capacity coefficient vectors

This module establishes the representation boundary between mathematical polynomials and the total fixed-capacity vectors used by Chapter 30's algorithms.

              namespace CLRSnamespace Chapter30open Polynomial

A total coefficient vector with fixed capacity n.

abbrev CoeffVector (K : Type*) (n : Nat) := Fin n → K

A coefficient vector whose capacity is a power of two.

abbrev PowTwoVec (K : Type*) (k : Nat) := CoeffVector K (2 ^ k)

Read and zero-pad the first n coefficients of a polynomial.

def coeffVector [Semiring K] (n : Nat) (p : K[X]) : CoeffVector K n :=
  fun i => p.coeff i

Reconstruct a polynomial from every slot of a fixed coefficient vector.

noncomputable def vectorToPolynomial [Semiring K] {n : Nat}
    (a : CoeffVector K n) : K[X] :=
  ∑ i : Fin n, Polynomial.monomial i.1 (a i)

Reconstruction preserves every coefficient whose index is in range.


theorem vectorToPolynomial_coeff [Semiring K] {n : Nat}
    (a : CoeffVector K n) (i : Fin n) :
    (vectorToPolynomial a).coeff i = a i := by
  classical
  change (Polynomial.lcoeff K i)
      (∑ j : Fin n, Polynomial.monomial j.1 (a j)) = a i
  rw [map_sum]
  simp only [Polynomial.lcoeff_apply, Polynomial.coeff_monomial]
  rw [Finset.sum_eq_single i]
  · simp
  · intro j _ hji
    rw [if_neg]
    exact fun hval => hji (Fin.ext hval)
  · simp

Reading the coefficients of a reconstructed vector returns that vector.

theorem coeffVector_vectorToPolynomial [Semiring K] {n : Nat}
    (a : CoeffVector K n) :
    coeffVector n (vectorToPolynomial a) = a := by
  funext i
  exact vectorToPolynomial_coeff a i

A reconstructed vector has no coefficient at or beyond its capacity.


theorem vectorToPolynomial_coeff_eq_zero_of_ge [Semiring K] {n i : Nat}
    (a : CoeffVector K n) (hi : n ≤ i) :
    (vectorToPolynomial a).coeff i = 0 := by
  classical
  have hne : ∀ j : Fin n, (j : Nat) ≠ i := by
    intro j hji
    omega
  simp [vectorToPolynomial, Polynomial.coeff_monomial, hne]

The degree of a reconstructed vector is strictly below its capacity.


theorem vectorToPolynomial_degree_lt [Semiring K] {n : Nat}
    (a : CoeffVector K n) :
    (vectorToPolynomial a).degree < n := by
  rw [Polynomial.degree_lt_iff_coeff_zero]
  intro i hi
  exact vectorToPolynomial_coeff_eq_zero_of_ge a hi

Reconstruction after truncation is exact when the polynomial fits.


theorem vectorToPolynomial_coeffVector [Semiring K] {n : Nat} (p : K[X])
    (hp : p.degree < n) :
    vectorToPolynomial (coeffVector n p) = p := by
  ext i
  by_cases hi : i < n
  · let j : Fin n := ⟨i, hi⟩
    simpa [coeffVector, j] using
      (vectorToPolynomial_coeff (coeffVector n p) j)
  · rw [vectorToPolynomial_coeff_eq_zero_of_ge]
    · exact ((Polynomial.degree_lt_iff_coeff_zero p n).mp hp) i
        (Nat.le_of_not_gt hi) |>.symm
    · exact Nat.le_of_not_gt hi

Remove the constant slot from a nonempty low-coefficient-first vector.

def tailCoeffs {K : Type*} {n : Nat} (a : CoeffVector K (n + 1)) :
    CoeffVector K n :=
  fun i => a i.succ

The value and arithmetic counters produced by a scalar computation.

The computed scalar.

The number of charged additions.

The number of charged multiplications.

              structure ArithmeticExecution (K : Type*) where  value : K  additions : Nat  multiplications : Nat

Total charged arithmetic work of a scalar execution.

def ArithmeticExecution.work (r : ArithmeticExecution K) : Nat :=
  r.additions + r.multiplications

Canonical Horner execution on a low-coefficient-first vector.

def hornerEvalExec [Semiring K] :
    {n : Nat} → CoeffVector K n → K → ArithmeticExecution K
  | 0, _, _ => ⟨0, 0, 0⟩
  | Variable name `n` is not explicitly referenced.

The binding can be removed (if unused) or named `_` (if used implicitly).

Note: This linter can be disabled with `set_option linter.unusedVariables false`n + 1, a, x =>
      let child := hornerEvalExec (tailCoeffs a) x
      ⟨a 0 + x * child.value,
        child.additions + 1,
        child.multiplications + 1⟩

The value returned by the canonical Horner execution.

def hornerEval [Semiring K] {n : Nat} (a : CoeffVector K n) (x : K) : K :=
  (hornerEvalExec a x).value

Reconstructing a nonempty vector splits into its constant term and shifted tail polynomial.

theorem vectorToPolynomial_succ [CommSemiring K] {n : Nat}
    (a : CoeffVector K (n + 1)) :
    vectorToPolynomial a = Polynomial.monomial 0 (a 0) +
      Polynomial.X * vectorToPolynomial (tailCoeffs a) := by
  simp [vectorToPolynomial, tailCoeffs, Fin.sum_univ_succ, Finset.mul_sum,
    Polynomial.X, Polynomial.monomial_mul_monomial, Nat.add_comm]

Evaluation of a nonempty coefficient vector splits into its constant term and the shifted tail.


theorem vectorToPolynomial_eval_succ [CommSemiring K] {n : Nat}
    (a : CoeffVector K (n + 1)) (x : K) :
    (vectorToPolynomial a).eval x =
      a 0 + x * (vectorToPolynomial (tailCoeffs a)).eval x := by
  rw [vectorToPolynomial_succ]
  simp

Horner execution evaluates the polynomial represented by its input.


theorem hornerEval_correct [CommSemiring K] {n : Nat}
    (a : CoeffVector K n) (x : K) :
    hornerEval a x = (vectorToPolynomial a).eval x := by
  induction n with
  | zero => simp [hornerEval, hornerEvalExec, vectorToPolynomial]
  | succ n ih =>
      simp only [hornerEval, hornerEvalExec]
      change a 0 + x * hornerEval (tailCoeffs a) x =
        (vectorToPolynomial a).eval x
      rw [ih (tailCoeffs a)]
      exact (vectorToPolynomial_eval_succ a x).symm

Horner execution charges exactly one addition per input slot.


theorem hornerEvalExec_additions [Semiring K] {n : Nat}
    (a : CoeffVector K n) (x : K) :
    (hornerEvalExec a x).additions = n := by
  induction n with
  | zero => rfl
  | succ n ih =>
      simp only [hornerEvalExec]
      rw [ih (tailCoeffs a)]

Horner execution charges exactly one multiplication per input slot.


theorem hornerEvalExec_multiplications [Semiring K] {n : Nat}
    (a : CoeffVector K n) (x : K) :
    (hornerEvalExec a x).multiplications = n := by
  induction n with
  | zero => rfl
  | succ n ih =>
      simp only [hornerEvalExec]
      rw [ih (tailCoeffs a)]

Horner execution performs exactly twice the vector capacity in charged arithmetic operations.


theorem hornerEvalWork_exact [Semiring K] {n : Nat}
    (a : CoeffVector K n) (x : K) :
    (hornerEvalExec a x).work = 2 * n := by
  rw [ArithmeticExecution.work, hornerEvalExec_additions,
    hornerEvalExec_multiplications]
  omega

end Chapter30end CLRS

CLRSLean.FourthEdition.Chapter_30.Section_30_1_Representing_Polynomials.S2_PointValueInterpolation

Chapter 30.1: Point-value interpolation

Point-value vectors are connected to Mathlib's Lagrange interpolant. The public theorems keep the distinct-node and degree-capacity premises explicit.

              namespace CLRSnamespace Chapter30open Polynomial

Evaluate a polynomial at every node in a fixed vector.

def pointValues [Semiring K] {n : Nat} (points : Fin n → K) (p : K[X]) :
    CoeffVector K n :=
  fun i => p.eval (points i)

The Lagrange interpolant through a fixed vector of nodes and values.

noncomputable def interpolateVector [Field K] {n : Nat}
    (points values : Fin n → K) : K[X] :=
  Lagrange.interpolate Finset.univ points values

Two degree-bounded polynomials agreeing at distinct nodes are equal.

theorem pointValues_injective [Field K] {n : Nat}
    {points : Fin n → K} (hpoints : Function.Injective points)
    {p q : K[X]} (hp : p.degree < n) (hq : q.degree < n)
    (hvalues : pointValues points p = pointValues points q) : p = q := by
  apply Polynomial.eq_of_degrees_lt_of_eval_index_eq Finset.univ
      hpoints.injOn
  · simpa using hp
  · simpa using hq
  · intro i _
    exact congrFun hvalues i

The Lagrange interpolant assumes its prescribed value at every distinct sample node.

theorem interpolate_pointValues [Field K] {n : Nat}
    {points values : Fin n → K} (hpoints : Function.Injective points)
    (i : Fin n) :
    (interpolateVector points values).eval (points i) = values i := by
  exact Lagrange.eval_interpolate_at_node values hpoints.injOn (by simp)

Every Lagrange basis divisor has natural degree at most one.

private theorem basisDivisor_natDegree_le_one [Field K] (x y : K) :
    (Lagrange.basisDivisor x y).natDegree ≤ 1 := by
  by_cases hxy : x = y
  · simp [hxy, Lagrange.basisDivisor_self]
  · simp [Lagrange.natDegree_basisDivisor_of_ne hxy]

A Lagrange basis polynomial has natural degree at most the number of factors in its defining product.


private theorem lagrangeBasis_natDegree_le [Field K] {ι : Type*}
    [DecidableEq ι] (s : Finset ι) (points : ι → K) (i : ι) :
    (Lagrange.basis s points i).natDegree ≤ (s.erase i).card := by
  rw [Lagrange.basis]
  calc
    (∏ j ∈ s.erase i, Lagrange.basisDivisor (points i) (points j)).natDegree
        ≤ ∑ j ∈ s.erase i,
            (Lagrange.basisDivisor (points i) (points j)).natDegree :=
      Polynomial.natDegree_prod_le _ _
    _ ≤ ∑ _j ∈ s.erase i, 1 := by
      exact Finset.sum_le_sum fun j _ =>
        basisDivisor_natDegree_le_one (points i) (points j)
    _ = (s.erase i).card := by simp

The interpolant always fits in the declared node capacity, independently of whether the nodes are distinct.


theorem interpolateVector_degree_lt [Field K] {n : Nat}
    (points values : Fin n → K) :
    (interpolateVector points values).degree < n := by
  cases n with
  | zero =>
      simp [interpolateVector, This simp argument is unused:
  Lagrange.interpolate_empty

Hint: Omit it from the simp argument list.
  simp [interpolateVector,̵ ̵L̵a̵g̵r̵a̵n̵g̵e̵.̵i̵n̵t̵e̵r̵p̵o̵l̵a̵t̵e̵_̵e̵m̵p̵t̵y̵]

Note: This linter can be disabled with `set_option linter.unusedSimpArgs false`Lagrange.interpolate_empty]
  | succ n =>
      have hnat : (interpolateVector points values).natDegree ≤ n := by
        rw [interpolateVector, Lagrange.interpolate_apply]
        apply Polynomial.natDegree_sum_le_of_forall_le
        intro i hi
        calc
          (Polynomial.C (values i) *
              Lagrange.basis Finset.univ points i).natDegree
              ≤ (Polynomial.C (values i)).natDegree +
                  (Lagrange.basis Finset.univ points i).natDegree :=
            Polynomial.natDegree_mul_le
          _ ≤ 0 + (Finset.univ.erase i).card := by
            gcongr
            · simp
            · exact lagrangeBasis_natDegree_le Finset.univ points i
          _ = n := by
            rw [Finset.card_erase_of_mem hi]
            simp
      calc
        (interpolateVector points values).degree ≤
            ((interpolateVector points values).natDegree : WithBot Nat) :=
          Polynomial.degree_le_natDegree
        _ ≤ (n : WithBot Nat) := by exact_mod_cast hnat
        _ < ((n + 1 : Nat) : WithBot Nat) := by exact_mod_cast Nat.lt_succ_self n

A degree-bounded polynomial with prescribed values is the interpolant.


theorem interpolate_unique [Field K] {n : Nat}
    {points values : Fin n → K} (hpoints : Function.Injective points)
    {p : K[X]} (hp : p.degree < n)
    (heval : ∀ i, p.eval (points i) = values i) :
    p = interpolateVector points values := by
  apply pointValues_injective hpoints hp
    (interpolateVector_degree_lt points values)
  funext i
  rw [pointValues, pointValues, heval i, interpolate_pointValues hpoints i]

Interpolating the point values of a fitting polynomial is a round trip.

theorem interpolate_pointValues_roundTrip [Field K] {n : Nat}
    {points : Fin n → K} (hpoints : Function.Injective points)
    {p : K[X]} (hp : p.degree < n) :
    interpolateVector points (pointValues points p) = p := by
  exact (interpolate_unique hpoints hp (fun _ => rfl)).symm

end Chapter30end CLRS

CLRSLean.FourthEdition.Chapter_30.Section_30_1_Representing_Polynomials.S3_RepresentationOperations

Chapter 30.1: Representation operations

This module gives canonical executions for fixed-vector operations. Its schoolbook multiplication really traverses every coefficient pair, inserts the product into one output bucket, and increments the attached counters.

              namespace CLRSnamespace Chapter30open Polynomial

The value and arithmetic counters produced by a fixed-vector operation.

The computed vector.

The number of charged additions.

The number of charged multiplications.

              structure VectorArithmeticExecution (K : Type*) (n : Nat) where  value : CoeffVector K n  additions : Nat  multiplications : Nat

Total charged arithmetic work of a vector execution.

def VectorArithmeticExecution.work (r : VectorArithmeticExecution K n) : Nat :=
  r.additions + r.multiplications

Canonical pointwise vector-addition execution.

def vectorAddExec [AddMonoid K] {n : Nat}
    (a b : CoeffVector K n) : VectorArithmeticExecution K n :=
  ⟨fun i => a i + b i, n, 0⟩

The value returned by canonical vector addition.

def vectorAdd [AddMonoid K] {n : Nat}
    (a b : CoeffVector K n) : CoeffVector K n :=
  (vectorAddExec a b).value

Canonical pointwise vector-multiplication execution.

def pointwiseMulExec [Mul K] {n : Nat}
    (a b : CoeffVector K n) : VectorArithmeticExecution K n :=
  ⟨fun i => a i * b i, 0, n⟩

The value returned by canonical pointwise multiplication.

def pointwiseMul [Mul K] {n : Nat}
    (a b : CoeffVector K n) : CoeffVector K n :=
  (pointwiseMulExec a b).value

Vector addition charges exactly one addition per slot.

theorem vectorAddWork_exact [AddMonoid K] {n : Nat}
    (a b : CoeffVector K n) :
    (vectorAddExec a b).work = n := by
  simp [vectorAddExec, VectorArithmeticExecution.work]

Pointwise multiplication charges exactly one multiplication per slot.

theorem pointwiseMulWork_exact [Mul K] {n : Nat}
    (a b : CoeffVector K n) :
    (pointwiseMulExec a b).work = n := by
  simp [pointwiseMulExec, VectorArithmeticExecution.work]

Vector addition represents polynomial addition.


theorem vectorToPolynomial_vectorAdd [CommSemiring K] {n : Nat}
    (a b : CoeffVector K n) :
    vectorToPolynomial (vectorAdd a b) =
      vectorToPolynomial a + vectorToPolynomial b := by
  ext i
  by_cases hi : i < n
  · let j : Fin n := ⟨i, hi⟩
    change (vectorToPolynomial (vectorAdd a b)).coeff j =
      (vectorToPolynomial a + vectorToPolynomial b).coeff j
    rw [Polynomial.coeff_add, vectorToPolynomial_coeff,
      vectorToPolynomial_coeff, vectorToPolynomial_coeff]
    rfl
  · have hge : n ≤ i := Nat.le_of_not_gt hi
    simp [vectorToPolynomial_coeff_eq_zero_of_ge, hge]

Sampling commutes with polynomial addition.

theorem pointValues_add [Semiring K] {n : Nat} (points : Fin n → K)
    (p q : K[X]) :
    pointValues points (p + q) =
      vectorAdd (pointValues points p) (pointValues points q) := by
  funext i
  simp [pointValues, vectorAdd, vectorAddExec]

Sampling commutes with polynomial multiplication.

theorem pointValues_mul [CommSemiring K] {n : Nat} (points : Fin n → K)
    (p q : K[X]) :
    pointValues points (p * q) =
      pointwiseMul (pointValues points p) (pointValues points q) := by
  funext i
  simp [pointValues, pointwiseMul, pointwiseMulExec]

The output bucket receiving the product of input slots i and j.

def productIndex {m n : Nat} (i : Fin m) (j : Fin n) : Fin (m + n) :=
  ⟨i.1 + j.1, by omega⟩

Add a scalar to one output bucket and leave every other bucket unchanged.

def addToBucket [AddMonoid K] {n : Nat} (out : CoeffVector K n)
    (i : Fin n) (v : K) : CoeffVector K n :=
  Function.update out i (out i + v)

A vector supported at exactly one output bucket.

def singleBucket [Zero K] {n : Nat} (i : Fin n) (v : K) : CoeffVector K n :=
  fun j => if j = i then v else 0

Updating one bucket is pointwise addition by its singleton vector.

theorem addToBucket_eq_vectorAdd_singleBucket [AddMonoid K] {n : Nat}
    (out : CoeffVector K n) (i : Fin n) (v : K) :
    addToBucket out i v = vectorAdd out (singleBucket i v) := by
  funext j
  by_cases hji : j = i
  · subst j
    simp [addToBucket, vectorAdd, vectorAddExec, singleBucket]
  · simp [addToBucket, vectorAdd, vectorAddExec, singleBucket, hji]

Reconstructing a singleton bucket gives the corresponding monomial.


theorem vectorToPolynomial_singleBucket [Semiring K] {n : Nat}
    (i : Fin n) (v : K) :
    vectorToPolynomial (singleBucket i v) = Polynomial.monomial i.1 v := by
  ext k
  by_cases hk : k < n
  · let j : Fin n := ⟨k, hk⟩
    simpa [singleBucket, j, Polynomial.coeff_monomial, Fin.ext_iff,
      eq_comm] using (vectorToPolynomial_coeff (singleBucket i v) j)
  · have hge : n ≤ k := Nat.le_of_not_gt hk
    have hik : (i : Nat) ≠ k := by omega
    rw [vectorToPolynomial_coeff_eq_zero_of_ge _ hge]
    simp [Polynomial.coeff_monomial, hik]

One bucket insertion adds exactly its corresponding monomial.


theorem vectorToPolynomial_addToBucket [CommSemiring K] {n : Nat}
    (out : CoeffVector K n) (i : Fin n) (v : K) :
    vectorToPolynomial (addToBucket out i v) =
      vectorToPolynomial out + Polynomial.monomial i.1 v := by
  rw [addToBucket_eq_vectorAdd_singleBucket,
    vectorToPolynomial_vectorAdd, vectorToPolynomial_singleBucket]

One coefficient-pair step of the schoolbook execution.

def schoolbookStep [Semiring K] {m n : Nat}
    (a : CoeffVector K m) (b : CoeffVector K n)
    (r : VectorArithmeticExecution K (m + n)) (ij : Fin m × Fin n) :
    VectorArithmeticExecution K (m + n) :=
  ⟨addToBucket r.value (productIndex ij.1 ij.2) (a ij.1 * b ij.2),
    r.additions + 1,
    r.multiplications + 1⟩

Traverse a list of coefficient pairs from an arbitrary execution state.

def schoolbookPairsExec [Semiring K] {m n : Nat}
    (a : CoeffVector K m) (b : CoeffVector K n)
    (pairs : List (Fin m × Fin n))
    (initial : VectorArithmeticExecution K (m + n)) :
    VectorArithmeticExecution K (m + n) :=
  pairs.foldl (schoolbookStep a b) initial

The zero-valued initial state of schoolbook multiplication.

def schoolbookInitial [Semiring K] (m n : Nat) :
    VectorArithmeticExecution K (m + n) :=
  ⟨fun _ => 0, 0, 0⟩

A deterministic list containing every coefficient-index pair exactly once, in lexicographic row order.

def coefficientPairs (m n : Nat) : List (Fin m × Fin n) :=
  (List.finRange m).flatMap fun i =>
    (List.finRange n).map fun j => (i, j)

The deterministic pair list enumerates the full Cartesian product.

theorem coefficientPairs_toFinset (m n : Nat) :
    (coefficientPairs m n).toFinset =
      (Finset.univ : Finset (Fin m)).product Finset.univ := by
  ext ij
  simp [coefficientPairs]

Summing along the deterministic pair list is the usual nested finite sum over both index types.


private theorem coefficientPairs_sum [AddCommMonoid M] {m n : Nat}
    (f : Fin m → Fin n → M) :
    ((coefficientPairs m n).map fun ij => f ij.1 ij.2).sum =
      ∑ i : Fin m, ∑ j : Fin n, f i j := by
  have hflat (xs : List (Fin m)) :
      (xs.flatMap fun i => (List.finRange n).map fun j => f i j).sum =
        (xs.map fun i => ((List.finRange n).map fun j => f i j).sum).sum := by
    induction xs with
    | nil => simp
    | cons i xs ih => simp [ih]
  have hinner (i : Fin m) :
      ((List.finRange n).map fun j => f i j).sum =
        ∑ j : Fin n, f i j := by
    rw [← List.sum_toFinset _ (List.nodup_finRange n)]
    simp
  rw [coefficientPairs]
  simp only [List.map_flatMap, List.map_map, Function.comp_def]
  rw [hflat]
  simp_rw [hinner]
  rw [← List.sum_toFinset _ (List.nodup_finRange m)]
  simp

Canonical schoolbook execution over every coefficient pair exactly once.

def schoolbookMulExec [Semiring K] {m n : Nat}
    (a : CoeffVector K m) (b : CoeffVector K n) :
    VectorArithmeticExecution K (m + n) :=
  schoolbookPairsExec a b (coefficientPairs m n) (schoolbookInitial m n)

The value returned by canonical schoolbook multiplication.

def schoolbookMul [Semiring K] {m n : Nat}
    (a : CoeffVector K m) (b : CoeffVector K n) : CoeffVector K (m + n) :=
  (schoolbookMulExec a b).value

Folding coefficient pairs adds their monomials to the initial polynomial.


private theorem schoolbookPairsExec_polynomial [CommSemiring K] {m n : Nat}
    (a : CoeffVector K m) (b : CoeffVector K n)
    (pairs : List (Fin m × Fin n))
    (initial : VectorArithmeticExecution K (m + n)) :
    vectorToPolynomial (schoolbookPairsExec a b pairs initial).value =
      vectorToPolynomial initial.value +
        (pairs.map fun ij => Polynomial.monomial (ij.1.1 + ij.2.1)
          (a ij.1 * b ij.2)).sum := by
  induction pairs generalizing initial with
  | nil => simp [schoolbookPairsExec]
  | cons ij pairs ih =>
      simp only [schoolbookPairsExec, List.foldl]
      change vectorToPolynomial
          (schoolbookPairsExec a b pairs (schoolbookStep a b initial ij)).value =
        vectorToPolynomial initial.value +
          (List.map (fun ij => Polynomial.monomial (ij.1.1 + ij.2.1)
            (a ij.1 * b ij.2)) (ij :: pairs)).sum
      rw [ih]
      simp [schoolbookStep, productIndex, vectorToPolynomial_addToBucket,
        add_assoc]

The full pair sum of coefficient monomials is the product of the two reconstructed input polynomials.


private theorem pairMonomialSum_eq [CommSemiring K] {m n : Nat}
    (a : CoeffVector K m) (b : CoeffVector K n) :
    (∑ i : Fin m, ∑ j : Fin n,
      Polynomial.monomial (i.1 + j.1) (a i * b j)) =
      vectorToPolynomial a * vectorToPolynomial b := by
  rw [vectorToPolynomial, vectorToPolynomial]
  simp only [Finset.sum_mul, Finset.mul_sum]
  rw [Finset.sum_comm]
  apply Finset.sum_congr rfl
  intro i _
  apply Finset.sum_congr rfl
  intro j _
  rw [Polynomial.monomial_mul_monomial]

Schoolbook multiplication represents the product of the input polynomials.


theorem schoolbookMul_correct [CommSemiring K] {m n : Nat}
    (a : CoeffVector K m) (b : CoeffVector K n) :
    vectorToPolynomial (schoolbookMul a b) =
      vectorToPolynomial a * vectorToPolynomial b := by
  rw [schoolbookMul, schoolbookMulExec]
  rw [schoolbookPairsExec_polynomial]
  rw [show vectorToPolynomial (schoolbookInitial m n).value = 0 by
    simp [schoolbookInitial, vectorToPolynomial]]
  simp only [zero_add]
  calc
    ((coefficientPairs m n).map fun ij =>
        Polynomial.monomial (ij.1.1 + ij.2.1) (a ij.1 * b ij.2)).sum =
        ∑ i : Fin m, ∑ j : Fin n,
          Polynomial.monomial (i.1 + j.1) (a i * b j) := by
      simpa using (coefficientPairs_sum (m := m) (n := n)
        (fun i j => Polynomial.monomial (i.1 + j.1) (a i * b j)))
    _ = vectorToPolynomial a * vectorToPolynomial b :=
      pairMonomialSum_eq a b

A schoolbook output always fits its declared sum capacity.

theorem schoolbookMul_degreeBound [Semiring K] {m n : Nat}
    (a : CoeffVector K m) (b : CoeffVector K n) :
    (vectorToPolynomial (schoolbookMul a b)).degree < m + n :=
  vectorToPolynomial_degree_lt _

Pair folding increments the addition counter once per processed pair.


private theorem schoolbookPairsExec_additions [Semiring K] {m n : Nat}
    (a : CoeffVector K m) (b : CoeffVector K n)
    (pairs : List (Fin m × Fin n))
    (initial : VectorArithmeticExecution K (m + n)) :
    (schoolbookPairsExec a b pairs initial).additions =
      initial.additions + pairs.length := by
  induction pairs generalizing initial with
  | nil => simp [schoolbookPairsExec]
  | cons ij pairs ih =>
      simp only [schoolbookPairsExec, List.foldl]
      change (schoolbookPairsExec a b pairs
        (schoolbookStep a b initial ij)).additions =
          initial.additions + (ij :: pairs).length
      rw [ih]
      simp [schoolbookStep]
      omega

Pair folding increments the multiplication counter once per pair.


private theorem schoolbookPairsExec_multiplications [Semiring K] {m n : Nat}
    (a : CoeffVector K m) (b : CoeffVector K n)
    (pairs : List (Fin m × Fin n))
    (initial : VectorArithmeticExecution K (m + n)) :
    (schoolbookPairsExec a b pairs initial).multiplications =
      initial.multiplications + pairs.length := by
  induction pairs generalizing initial with
  | nil => simp [schoolbookPairsExec]
  | cons ij pairs ih =>
      simp only [schoolbookPairsExec, List.foldl]
      change (schoolbookPairsExec a b pairs
        (schoolbookStep a b initial ij)).multiplications =
          initial.multiplications + (ij :: pairs).length
      rw [ih]
      simp [schoolbookStep]
      omega

Schoolbook execution performs exactly one addition per coefficient pair.


theorem schoolbookMulExec_additions [Semiring K] {m n : Nat}
    (a : CoeffVector K m) (b : CoeffVector K n) :
    (schoolbookMulExec a b).additions = m * n := by
  rw [schoolbookMulExec, schoolbookPairsExec_additions]
  simp [schoolbookInitial, coefficientPairs]

Schoolbook execution performs exactly one multiplication per coefficient pair.


theorem schoolbookMulExec_multiplications [Semiring K] {m n : Nat}
    (a : CoeffVector K m) (b : CoeffVector K n) :
    (schoolbookMulExec a b).multiplications = m * n := by
  rw [schoolbookMulExec, schoolbookPairsExec_multiplications]
  simp [schoolbookInitial, coefficientPairs]

Schoolbook execution performs exactly twice the number of coefficient pairs in charged arithmetic work.


theorem schoolbookMulWork_exact [Semiring K] {m n : Nat}
    (a : CoeffVector K m) (b : CoeffVector K n) :
    (schoolbookMulExec a b).work = 2 * (m * n) := by
  rw [VectorArithmeticExecution.work, schoolbookMulExec_additions,
    schoolbookMulExec_multiplications]
  omega

end Chapter30end CLRS